:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, XREAL_0, SUBSET_1, RCOMP_1, SEQ_1, PARTFUN1,
XXREAL_1, CARD_1, SIN_COS, ARYTM_3, TARSKI, ARYTM_1, XBOOLE_0, RELAT_1,
SIN_COS4, ORDINAL4, FUNCT_1, FDIFF_1, SQUARE_1, ORDINAL2, XXREAL_0,
VALUED_0, FCONT_1, SEQ_2, FUNCT_2, SINCOS10, ORDINAL1;
notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1,
SEQ_1, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, RFUNCT_2, FCONT_1,
XBOOLE_0, FDIFF_9, SEQ_2;
constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
SIN_COS, PARTFUN2, SIN_COS4, RELSET_1, FDIFF_9, SEQ_2, XXREAL_2, NEWTON,
COMSEQ_2;
registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
FUNCT_1, SIN_COS6, RFUNCT_2, ORDINAL1, INT_1, VALUED_0, XXREAL_2,
XBOOLE_0, NUMBERS, SIN_COS, SQUARE_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI;
equalities FDIFF_9, XCMPLX_0, RCOMP_1, SQUARE_1;
expansions TARSKI;
theorems SIN_COS6, FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG,
RFUNCT_2, FCONT_1, FUNCT_1, XBOOLE_0, SQUARE_1, FCONT_3, XREAL_1, TARSKI,
XBOOLE_1, ROLLE, RFUNCT_1, FCONT_2, SEQ_1, FDIFF_9, XXREAL_0, FUNCT_2,
XXREAL_1, XXREAL_2;
begin :: arcsec, arccosec
reserve x,x0, r,r1,r2 for Real,
th for Real,
rr for set,
rseq for Real_Sequence;
Lm1: [.0,PI/2.[ c= ].-PI/2,PI/2.[
proof
A1: 0 in ].-PI/2,PI/2.[;
A2: {0} c= ].-PI/2,PI/2.[
by A1,TARSKI:def 1;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then ].0,PI/2.[ \/ {0} c= ].-PI/2,PI/2.[ by A2,XBOOLE_1:8;
hence thesis by XXREAL_1:131;
end;
theorem Th1:
[.0,PI/2.[ c= dom sec
proof
[.0,PI/2.[ /\ cos"{0} = {}
proof
assume [.0,PI/2.[ /\ cos"{0} <> {};
then consider rr being object such that
A1: rr in [.0,PI/2.[ /\ cos"{0} by XBOOLE_0:def 1;
rr in cos"{0} by A1,XBOOLE_0:def 4;
then
A2: cos.(rr) in {0} by FUNCT_1:def 7;
rr in [.0,PI/2.[ by A1,XBOOLE_0:def 4;
then cos.rr <> 0 by Lm1,COMPTRIG:11;
hence contradiction by A2,TARSKI:def 1;
end;
then
[.0,PI/2.[ \ cos"{0} c= dom cos \ cos"{0} & [.0,PI/2.[ misses cos"{0} by
SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then [.0,PI/2.[ c= dom cos \ cos"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
Lm2: ].PI/2,PI.] c= ].PI/2,3/2*PI.[
proof
A1: PI/2 < PI/1 by XREAL_1:76;
A2: PI < 3/2*PI by XREAL_1:155;
then
A3: PI in ].PI/2,3/2*PI.[ by A1;
A4: {PI} c= ].PI/2,3/2*PI.[
by A3,TARSKI:def 1;
].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by A2,XXREAL_1:46;
then ].PI/2,PI.[ \/ {PI} c= ].PI/2,3/2*PI.[ by A4,XBOOLE_1:8;
hence thesis by A1,XXREAL_1:132;
end;
theorem Th2:
].PI/2,PI.] c= dom sec
proof
].PI/2,PI.] /\ cos"{0} = {}
proof
assume ].PI/2,PI.] /\ cos"{0} <> {};
then consider rr being object such that
A1: rr in ].PI/2,PI.] /\ cos"{0} by XBOOLE_0:def 1;
rr in cos"{0} by A1,XBOOLE_0:def 4;
then
A2: cos.(rr) in {0} by FUNCT_1:def 7;
rr in ].PI/2,PI.] by A1,XBOOLE_0:def 4;
then cos.rr <> 0 by Lm2,COMPTRIG:13;
hence contradiction by A2,TARSKI:def 1;
end;
then
].PI/2,PI.] \ cos"{0} c= dom cos \ cos"{0} & ].PI/2,PI.] misses cos"{0}
by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then ].PI/2,PI.] c= dom cos \ cos"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
Lm3: [.-PI/2,0.[ c= ].-PI,0.[
proof
PI/2 < PI/1 by XREAL_1:76;
then
A1: -PI < -PI/2 by XREAL_1:24;
then
A2: -PI/2 in ].-PI,0.[;
A3: {-PI/2} c= ].-PI,0.[
by A2,TARSKI:def 1;
].-PI/2,0.[ c= ].-PI,0.[ by A1,XXREAL_1:46;
then ].-PI/2,0.[ \/ {-PI/2} c= ].-PI,0.[ by A3,XBOOLE_1:8;
hence thesis by XXREAL_1:131;
end;
theorem Th3:
[.-PI/2,0.[ c= dom cosec
proof
[.-PI/2,0.[ /\ sin"{0} = {}
proof
assume [.-PI/2,0.[ /\ sin"{0} <> {};
then consider rr being object such that
A1: rr in [.-PI/2,0.[ /\ sin"{0} by XBOOLE_0:def 1;
A2: rr in sin"{0} by A1,XBOOLE_0:def 4;
A3: rr in [.-PI/2,0.[ by A1,XBOOLE_0:def 4;
reconsider rr as Real by A1;
rr < 0 by A3,Lm3,XXREAL_1:4;
then
A4: rr+2*PI < 0+2*PI by XREAL_1:8;
-PI < rr by A3,Lm3,XXREAL_1:4;
then -PI+2*PI < rr+2*PI by XREAL_1:8;
then rr+2*PI in ].PI,2*PI.[ by A4;
then sin.(rr+2*PI) < 0 by COMPTRIG:9;
then
A5: sin.rr <> 0 by SIN_COS:78;
sin.rr in {0} by A2,FUNCT_1:def 7;
hence contradiction by A5,TARSKI:def 1;
end;
then
[.-PI/2,0.[ \ sin"{0} c= dom sin \ sin"{0} & [.-PI/2,0.[ misses sin"{0}
by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then [.-PI/2,0.[ c= dom sin \ sin"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
Lm4: ].0,PI/2.] c= ].0,PI.[
proof
A1: PI/2 < PI/1 by XREAL_1:76;
then
A2: PI/2 in ].0,PI.[;
A3: {PI/2} c= ].0,PI.[
by A2,TARSKI:def 1;
].0,PI/2.[ c= ].0,PI.[ by A1,XXREAL_1:46;
then ].0,PI/2.[ \/ {PI/2} c= ].0,PI.[ by A3,XBOOLE_1:8;
hence thesis by XXREAL_1:132;
end;
theorem Th4:
].0,PI/2.] c= dom cosec
proof
].0,PI/2.] /\ sin"{0} = {}
proof
assume ].0,PI/2.] /\ sin"{0} <> {};
then consider rr being object such that
A1: rr in ].0,PI/2.] /\ sin"{0} by XBOOLE_0:def 1;
rr in sin"{0} by A1,XBOOLE_0:def 4;
then
A2: sin.rr in {0} by FUNCT_1:def 7;
rr in ].0,PI/2.] by A1,XBOOLE_0:def 4;
then sin.rr <> 0 by Lm4,COMPTRIG:7;
hence contradiction by A2,TARSKI:def 1;
end;
then
].0,PI/2.] \ sin"{0} c= dom sin \ sin"{0} & ].0,PI/2.] misses sin"{0} by
SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then ].0,PI/2.] c= dom sin \ sin"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
theorem Th5:
sec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
holds diff(sec,x) = sin.x/(cos.x)^2
proof
set Z = ].0,PI/2.[;
[.0,PI/2.[ = Z \/ {0} by XXREAL_1:131;
then Z c= [.0,PI/2.[ by XBOOLE_1:7;
then
A1: Z c= dom sec by Th1;
then
A2: sec is_differentiable_on Z by FDIFF_9:4;
for x st x in Z holds diff(sec,x) = sin.x/(cos.x)^2
proof
let x;
assume
A3: x in Z;
then diff(sec,x) = ((sec)`|Z).x by A2,FDIFF_1:def 7
.= sin.x/(cos.x)^2 by A1,A3,FDIFF_9:4;
hence thesis;
end;
hence thesis by A1,FDIFF_9:4;
end;
theorem Th6:
sec is_differentiable_on ].PI/2,PI.[ & for x st x in ].PI/2,PI.[
holds diff(sec,x) = sin.x/(cos.x)^2
proof
set Z = ].PI/2,PI.[;
PI/2 < PI/1 by XREAL_1:76;
then ].PI/2,PI.] = Z \/ {PI} by XXREAL_1:132;
then Z c= ].PI/2,PI.] by XBOOLE_1:7;
then
A1: Z c= dom sec by Th2;
then
A2: sec is_differentiable_on Z by FDIFF_9:4;
for x st x in Z holds diff(sec,x) = sin.x/(cos.x)^2
proof
let x;
assume
A3: x in Z;
then diff(sec,x) = ((sec)`|Z).x by A2,FDIFF_1:def 7
.= sin.x/(cos.x)^2 by A1,A3,FDIFF_9:4;
hence thesis;
end;
hence thesis by A1,FDIFF_9:4;
end;
theorem Th7:
cosec is_differentiable_on ].-PI/2,0.[ & for x st x in ].-PI/2,0
.[ holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
set Z = ].-PI/2,0.[;
[.-PI/2,0.[ = Z \/ {-PI/2} by XXREAL_1:131;
then Z c= [.-PI/2,0.[ by XBOOLE_1:7;
then
A1: Z c= dom cosec by Th3;
then
A2: cosec is_differentiable_on Z by FDIFF_9:5;
for x st x in Z holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
let x;
assume
A3: x in Z;
then diff(cosec,x) = ((cosec)`|Z).x by A2,FDIFF_1:def 7
.= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
hence thesis;
end;
hence thesis by A1,FDIFF_9:5;
end;
theorem Th8:
cosec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
set Z = ].0,PI/2.[;
].0,PI/2.] = Z \/ {PI/2} by XXREAL_1:132;
then Z c= ].0,PI/2.] by XBOOLE_1:7;
then
A1: Z c= dom cosec by Th4;
then
A2: cosec is_differentiable_on Z by FDIFF_9:5;
for x st x in Z holds diff(cosec,x) = -cos.x/(sin.x)^2
proof
let x;
assume
A3: x in Z;
then diff(cosec,x) = ((cosec)`|Z).x by A2,FDIFF_1:def 7
.= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
hence thesis;
end;
hence thesis by A1,FDIFF_9:5;
end;
theorem
sec|].0,PI/2.[ is continuous by Th5,FDIFF_1:25;
theorem
sec|].PI/2,PI.[ is continuous by Th6,FDIFF_1:25;
theorem
cosec|].-PI/2,0.[ is continuous by Th7,FDIFF_1:25;
theorem
cosec|].0,PI/2.[ is continuous by Th8,FDIFF_1:25;
Lm5: 0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[
proof
PI/4 < PI/2 by XREAL_1:76;
hence thesis;
end;
Lm6: 3/4*PI in ].PI/2,PI.] & PI in ].PI/2,PI.]
proof
PI/4 < PI/2 by XREAL_1:76;
then PI/4+PI/2 > 0+PI/2 & PI/4+PI/2 < PI/2+PI/2 by XREAL_1:8;
hence thesis by COMPTRIG:5;
end;
Lm7: -PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[
proof
PI/4 < PI/2 by XREAL_1:76;
then -PI/4 > -PI/2 by XREAL_1:24;
hence thesis;
end;
Lm8: PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.]
proof
PI/4 < PI/2 by XREAL_1:76;
hence thesis;
end;
Lm9: ].0,PI/2.[ c= [.0,PI/2.[ by XXREAL_1:22;
then
Lm10: ].0,PI/2.[ c= dom sec by Th1;
Lm11: ].PI/2,PI.[ c= ].PI/2,PI.] by XXREAL_1:21;
then
Lm12: ].PI/2,PI.[ c= dom sec by Th2;
Lm13: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
Lm14: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
Lm15: ].-PI/2,0.[ c= [.-PI/2,0.[ by XXREAL_1:22;
then
Lm16: ].-PI/2,0.[ c= dom cosec by Th3;
Lm17: ].0,PI/2.[ c= ].0,PI/2.] by XXREAL_1:21;
then
Lm18: ].0,PI/2.[ c= dom cosec by Th4;
Lm19: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
Lm20: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
].0,PI/2.[ = dom(sec|].0,PI/2.[) by Lm9,Th1,RELAT_1:62,XBOOLE_1:1;
then
Lm21: ].0,PI/2.[ c= dom(sec|[.0,PI/2.[|].0,PI/2.[) by RELAT_1:74,XXREAL_1:22;
].PI/2,PI.[ = dom(sec|].PI/2,PI.[) by Lm11,Th2,RELAT_1:62,XBOOLE_1:1;
then
Lm22: ].PI/2,PI.[ c= dom(sec|].PI/2,PI.]|].PI/2,PI.[) by RELAT_1:74,XXREAL_1:21
;
].-PI/2,0.[ = dom(cosec|].-PI/2,0.[) by Lm15,Th3,RELAT_1:62,XBOOLE_1:1;
then
Lm23: ].-PI/2,0.[ c= dom(cosec|[.-PI/2,0.[|].-PI/2,0.[) by RELAT_1:74
,XXREAL_1:22;
].0,PI/2.[ = dom(cosec|].0,PI/2.[) by Lm17,Th4,RELAT_1:62,XBOOLE_1:1;
then
Lm24: ].0,PI/2.[ c= dom(cosec|].0,PI/2.]|].0,PI/2.[) by RELAT_1:74,XXREAL_1:21;
theorem Th13:
sec|].0,PI/2.[ is increasing
proof
for x st x in ].0,PI/2.[ holds diff(sec,x) > 0
proof
let x;
assume
A1: x in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A2: cos.x > 0 by A1,COMPTRIG:11;
PI/2 < PI/1 by XREAL_1:76;
then ].0,PI/2.[ c= ].0,PI.[ by XXREAL_1:46;
then sin.x > 0 by A1,COMPTRIG:7;
then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A2;
hence thesis by A1,Th5;
end;
hence thesis by Lm9,Th1,Th5,ROLLE:9,XBOOLE_1:1;
end;
theorem Th14:
sec|].PI/2,PI.[ is increasing
proof
for x st x in ].PI/2,PI.[ holds diff(sec,x) > 0
proof
let x;
assume
A1: x in ].PI/2,PI.[;
PI <= 3/2*PI by XREAL_1:151;
then ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by XXREAL_1:46;
then
A2: cos.x < 0 by A1,COMPTRIG:13;
].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;
then sin.x > 0 by A1,COMPTRIG:7;
then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A2;
hence thesis by A1,Th6;
end;
hence thesis by Lm11,Th2,Th6,ROLLE:9,XBOOLE_1:1;
end;
theorem Th15:
cosec|].-PI/2,0.[ is decreasing
proof
for x st x in ].-PI/2,0.[ holds diff(cosec,x) < 0
proof
let x;
assume
A1: x in ].-PI/2,0.[;
then x < 0 by XXREAL_1:4;
then
A2: x+2*PI < 0+2*PI by XREAL_1:8;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by XXREAL_1:131;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3;
then -PI < x by A1,XXREAL_1:4;
then -PI+2*PI < x+2*PI by XREAL_1:8;
then x+2*PI in ].PI,2*PI.[ by A2;
then sin.(x+2*PI) < 0 by COMPTRIG:9;
then
A3: sin.x < 0 by SIN_COS:78;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then cos.x > 0 by A1,COMPTRIG:11;
then -cos.x/(sin.x)^2 < -0 by A3;
hence thesis by A1,Th7;
end;
hence thesis by Lm15,Th3,Th7,ROLLE:10,XBOOLE_1:1;
end;
theorem Th16:
cosec|].0,PI/2.[ is decreasing
proof
for x st x in ].0,PI/2.[ holds diff(cosec,x) < 0
proof
let x;
assume
A1: x in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A2: cos.x > 0 by A1,COMPTRIG:11;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
then sin.x > 0 by A1,COMPTRIG:7;
then -cos.x/(sin.x)^2 < -0 by A2;
hence thesis by A1,Th8;
end;
hence thesis by Lm17,Th4,Th8,ROLLE:10,XBOOLE_1:1;
end;
theorem Th17:
sec|[.0,PI/2.[ is increasing
proof
now
let r1,r2;
assume that
A1: r1 in [.0,PI/2.[ /\ dom sec and
A2: r2 in [.0,PI/2.[ /\ dom sec and
A3: r1 < r2;
A4: r1 in dom sec by A1,XBOOLE_0:def 4;
A5: r1 in [.0,PI/2.[ by A1,XBOOLE_0:def 4;
then
A6: r1 < PI/2 by XXREAL_1:3;
A7: r2 in dom sec by A2,XBOOLE_0:def 4;
A8: r2 in [.0,PI/2.[ by A2,XBOOLE_0:def 4;
then
A9: r2 < PI/2 by XXREAL_1:3;
now
per cases by A5,XXREAL_1:3;
suppose
A10: 0 = r1;
r2 < PI/2 & PI/2 < 2*PI by A8,Lm1,XREAL_1:68,XXREAL_1:4;
then r2 < 2*PI by XXREAL_0:2;
then cos r2 < 1 by A3,A10,SIN_COS6:34;
then
A11: cos.r2 < 1 by SIN_COS:def 19;
-PI/2+2*PI*0 < r2 & r2 < PI/2+2*PI*0 by A8,Lm1,XXREAL_1:4;
then cos r2 > 0 by SIN_COS6:13;
then cos.r2 > 0 by SIN_COS:def 19;
then
A12: 1/1 < 1/cos.r2 by A11,XREAL_1:76;
sec.r1 = 1/1 by A4,A10,RFUNCT_1:def 2,SIN_COS:30
.= 1;
hence sec.r2 > sec.r1 by A7,A12,RFUNCT_1:def 2;
end;
suppose
A13: 0 < r1;
then r1 in ].0,PI/2.[ by A6;
then
A14: r1 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 4;
r2 in ].0,PI/2.[ by A3,A9,A13;
then r2 in ].0,PI/2.[ /\ dom sec by A7,XBOOLE_0:def 4;
hence sec.r2 > sec.r1 by A3,A14,Th13,RFUNCT_2:20;
end;
end;
hence sec.r2 > sec.r1;
end;
hence thesis by RFUNCT_2:20;
end;
theorem Th18:
sec|].PI/2,PI.] is increasing
proof
now
let r1,r2;
assume that
A1: r1 in ].PI/2,PI.] /\ dom sec and
A2: r2 in ].PI/2,PI.] /\ dom sec and
A3: r1 < r2;
A4: r1 in dom sec by A1,XBOOLE_0:def 4;
A5: r2 in dom sec by A2,XBOOLE_0:def 4;
A6: r1 in ].PI/2,PI.] by A1,XBOOLE_0:def 4;
then
A7: PI/2 < r1 by XXREAL_1:2;
A8: r2 in ].PI/2,PI.] by A2,XBOOLE_0:def 4;
then
A9: r2 <= PI by XXREAL_1:2;
A10: PI/2 < r2 by A8,XXREAL_1:2;
now
per cases by A9,XXREAL_0:1;
suppose
A11: r2 < PI;
then r1 < PI by A3,XXREAL_0:2;
then r1 in ].PI/2,PI.[ by A7;
then
A12: r1 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 4;
r2 in ].PI/2,PI.[ by A10,A11;
then r2 in ].PI/2,PI.[ /\ dom sec by A5,XBOOLE_0:def 4;
hence sec.r2 > sec.r1 by A3,A12,Th14,RFUNCT_2:20;
end;
suppose
A13: r2 = PI;
PI*1 < PI*(3/2) by XREAL_1:68;
then
A14: r1 < 3/2*PI+2*PI*0 by A3,A13,XXREAL_0:2;
PI/2+2*PI*0 < r1 by A6,XXREAL_1:2;
then cos r1 < 0 by A14,SIN_COS6:14;
then
A15: cos.r1 < 0 by SIN_COS:def 19;
r1 < PI by A3,A9,XXREAL_0:2;
then cos r1 > -1 by A7,SIN_COS6:35;
then cos.r1 > -1 by SIN_COS:def 19;
then
A16: (cos.r1)" < (-1)" by A15,XREAL_1:87;
sec.r2 = 1/(-1) by A5,A13,RFUNCT_1:def 2,SIN_COS:76
.= -1;
hence sec.r1 < sec.r2 by A4,A16,RFUNCT_1:def 2;
end;
end;
hence sec.r2 > sec.r1;
end;
hence thesis by RFUNCT_2:20;
end;
theorem Th19:
cosec|[.-PI/2,0.[ is decreasing
proof
now
let r1,r2;
assume that
A1: r1 in [.-PI/2,0.[ /\ dom cosec and
A2: r2 in [.-PI/2,0.[ /\ dom cosec and
A3: r1 < r2;
A4: r1 in dom cosec by A1,XBOOLE_0:def 4;
A5: r1 in [.-PI/2,0.[ by A1,XBOOLE_0:def 4;
then
A6: r1 < 0 by XXREAL_1:3;
A7: r2 in dom cosec by A2,XBOOLE_0:def 4;
A8: r2 in [.-PI/2,0.[ by A2,XBOOLE_0:def 4;
then
A9: r2 < 0 by XXREAL_1:3;
A10: -PI/2 <= r1 by A5,XXREAL_1:3;
now
per cases by A10,XXREAL_0:1;
suppose
A11: -PI/2 = r1;
-PI/2 > -PI by COMPTRIG:5,XREAL_1:24;
then
A12: ].-PI/2,0.[ c= ].-PI,0.[ by XXREAL_1:46;
r2 in ].-PI/2,0.[ by A3,A9,A11;
then -PI < r2 by A12,XXREAL_1:4;
then
A13: -PI+2*PI < r2+2*PI by XREAL_1:8;
r2+2*PI < 0+2*PI by A9,XREAL_1:8;
then r2+2*PI in ].PI,2*PI.[ by A13;
then sin.(r2+2*PI) < 0 by COMPTRIG:9;
then
A14: sin.r2 < 0 by SIN_COS:78;
A15: r2 < 2*PI+2*PI*(-1) by A8,XXREAL_1:3;
3/2*PI+2*PI*(-1) < r2 by A3,A11;
then sin r2 > -1 by A15,SIN_COS6:39;
then sin.r2 > -1 by SIN_COS:def 17;
then
A16: (sin.r2)" < (-1)" by A14,XREAL_1:87;
cosec.r1 = 1/sin.(-PI/2) by A4,A11,RFUNCT_1:def 2
.= 1/(-1) by SIN_COS:30,76
.= -1;
hence cosec.r2 < cosec.r1 by A7,A16,RFUNCT_1:def 2;
end;
suppose
A17: -PI/2 < r1;
then -PI/2 < r2 by A3,XXREAL_0:2;
then r2 in ].-PI/2,0.[ by A9;
then
A18: r2 in ].-PI/2,0.[ /\ dom cosec by A7,XBOOLE_0:def 4;
r1 in ].-PI/2,0.[ by A6,A17;
then r1 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 4;
hence cosec.r2 < cosec.r1 by A3,A18,Th15,RFUNCT_2:21;
end;
end;
hence cosec.r2 < cosec.r1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem Th20:
cosec|].0,PI/2.] is decreasing
proof
now
let r1,r2;
assume that
A1: r1 in ].0,PI/2.] /\ dom cosec and
A2: r2 in ].0,PI/2.] /\ dom cosec and
A3: r1 < r2;
A4: r1 in dom cosec by A1,XBOOLE_0:def 4;
A5: r2 in ].0,PI/2.] by A2,XBOOLE_0:def 4;
then
A6: r2 <= PI/2 by XXREAL_1:2;
A7: r2 in dom cosec by A2,XBOOLE_0:def 4;
A8: r1 in ].0,PI/2.] by A1,XBOOLE_0:def 4;
then
A9: 0 < r1 by XXREAL_1:2;
A10: 0 < r2 by A5,XXREAL_1:2;
now
per cases by A6,XXREAL_0:1;
suppose
A11: r2 < PI/2;
then r1 < PI/2 by A3,XXREAL_0:2;
then r1 in ].0,PI/2.[ by A9;
then
A12: r1 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 4;
r2 in ].0,PI/2.[ by A10,A11;
then r2 in ].0,PI/2.[ /\ dom cosec by A7,XBOOLE_0:def 4;
hence cosec.r2 < cosec.r1 by A3,A12,Th16,RFUNCT_2:21;
end;
suppose
A13: r2 = PI/2;
then sin r1 < 1 by A3,A9,SIN_COS6:30;
then
A14: sin.r1 < 1 by SIN_COS:def 17;
sin.r1 > 0 by A8,Lm4,COMPTRIG:7;
then
A15: 1/1 < 1/sin.r1 by A14,XREAL_1:76;
cosec.r2 = 1/1 by A7,A13,RFUNCT_1:def 2,SIN_COS:76
.= 1;
hence cosec.r2 < cosec.r1 by A4,A15,RFUNCT_1:def 2;
end;
end;
hence cosec.r2 < cosec.r1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem
sec | [.0,PI/2.[ is one-to-one by Th17,FCONT_3:8;
theorem
sec | ].PI/2,PI.] is one-to-one by Th18,FCONT_3:8;
theorem
cosec | [.-PI/2,0.[ is one-to-one by Th19,FCONT_3:8;
theorem
cosec | ].0,PI/2.] is one-to-one by Th20,FCONT_3:8;
registration
cluster sec | [.0,PI/2.[ -> one-to-one;
coherence by Th17,FCONT_3:8;
cluster sec | ].PI/2,PI.] -> one-to-one;
coherence by Th18,FCONT_3:8;
cluster cosec | [.-PI/2,0.[ -> one-to-one;
coherence by Th19,FCONT_3:8;
cluster cosec | ].0,PI/2.] -> one-to-one;
coherence by Th20,FCONT_3:8;
end;
definition
func arcsec1 -> PartFunc of REAL, REAL equals
(sec | [.0,PI/2.[)";
coherence;
func arcsec2 -> PartFunc of REAL, REAL equals
(sec | ].PI/2, PI.])";
coherence;
func arccosec1 -> PartFunc of REAL, REAL equals
(cosec | [.-PI/2,0.[)";
coherence;
func arccosec2 -> PartFunc of REAL, REAL equals
(cosec | ].0,PI/2.])";
coherence;
end;
definition
let r be Real;
func arcsec1 r -> number equals
arcsec1.r;
coherence;
func arcsec2 r -> number equals
arcsec2.r;
coherence;
func arccosec1 r -> number equals
arccosec1.r;
coherence;
func arccosec2 r -> number equals
arccosec2.r;
coherence;
end;
registration
let r be Real;
cluster arcsec1 r -> real;
coherence;
cluster arcsec2 r -> real;
coherence;
cluster arccosec1 r -> real;
coherence;
cluster arccosec2 r -> real;
coherence;
end;
Lm25: (arcsec1 qua Function)" = sec | [.0,PI/2.[ by FUNCT_1:43;
Lm26: (arcsec2 qua Function)" = sec | ].PI/2,PI.] by FUNCT_1:43;
Lm27: (arccosec1 qua Function)" = cosec | [.-PI/2,0.[ by FUNCT_1:43;
Lm28: (arccosec2 qua Function)" = cosec | ].0,PI/2.] by FUNCT_1:43;
theorem Th25:
rng arcsec1 = [.0,PI/2.[
proof
dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
hence thesis by FUNCT_1:33;
end;
theorem Th26:
rng arcsec2 = ].PI/2,PI.]
proof
dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
hence thesis by FUNCT_1:33;
end;
theorem Th27:
rng arccosec1 = [.-PI/2,0.[
proof
dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
hence thesis by FUNCT_1:33;
end;
theorem Th28:
rng arccosec2 = ].0,PI/2.]
proof
dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
hence thesis by FUNCT_1:33;
end;
registration
cluster arcsec1 -> one-to-one;
coherence;
cluster arcsec2 -> one-to-one;
coherence;
cluster arccosec1 -> one-to-one;
coherence;
cluster arccosec2 -> one-to-one;
coherence;
end;
theorem Th29:
sin.(PI/4) = 1/sqrt 2 & cos.(PI/4) = 1/sqrt 2
proof
A1: (sqrt(1/2))^2 = 1/2 by SQUARE_1:def 2;
1 = (sin.(PI/4))^2 + (sin.(PI/4))^2 by SIN_COS:28,73
.= 2*(sin.(PI/4))^2;
then
A2: sin.(PI/4) = sqrt(1/2) or sin.(PI/4) = -sqrt(1/2) by A1,SQUARE_1:40;
PI/4 < PI/1 by XREAL_1:76;
then
A3: PI/4 in ].0,PI.[;
sqrt(1/2) > 0 by SQUARE_1:25;
hence thesis by A2,A3,COMPTRIG:7,SIN_COS:73,SQUARE_1:32;
end;
theorem Th30:
sin.(-PI/4) = -1/sqrt 2 & cos.(-PI/4) = 1/sqrt 2 & sin.(3/4*PI)
= 1/sqrt 2 & cos.(3/4*PI) = -1/sqrt 2
proof
A1: cos.(-PI/4) = 1/sqrt 2 by Th29,SIN_COS:30;
A2: cos.(3/4*PI) = cos.(PI+(-PI/4)) .= -1/sqrt 2 by A1,SIN_COS:78;
A3: sin.(-PI/4) = -1/sqrt 2 by Th29,SIN_COS:30;
sin.(3/4*PI) = sin.(PI+(-PI/4)) .= -(-1/sqrt 2) by A3,SIN_COS:78
.= 1/sqrt 2;
hence thesis by A2,Th29,SIN_COS:30;
end;
theorem Th31:
sec.0 = 1 & sec.(PI/4) = sqrt 2 & sec.(3/4*PI) = -sqrt 2 & sec. PI = -1
proof
A1: sec.PI = 1/(-1) by Lm6,Th2,RFUNCT_1:def 2,SIN_COS:76
.= -1;
A2: sec.(3/4*PI) = 1/(-1/sqrt 2) by Lm6,Th2,Th30,RFUNCT_1:def 2
.= -1/(1/sqrt 2) by XCMPLX_1:188
.= -sqrt 2;
A3: sec.0 = 1/1 by Lm5,Th1,RFUNCT_1:def 2,SIN_COS:30
.= 1;
sec.(PI/4) = 1/(1/sqrt 2) by Lm5,Th1,Th29,RFUNCT_1:def 2
.= sqrt 2;
hence thesis by A3,A2,A1;
end;
theorem Th32:
cosec.(-PI/2) = -1 & cosec.(-PI/4) = -sqrt 2 & cosec.(PI/4) =
sqrt 2 & cosec.(PI/2) = 1
proof
A1: cosec.(PI/2) = 1/1 by Lm8,Th4,RFUNCT_1:def 2,SIN_COS:76
.= 1;
A2: cosec.(PI/4) = 1/(1/sqrt 2) by Lm8,Th4,Th29,RFUNCT_1:def 2
.= sqrt 2;
A3: cosec.(-PI/2) = 1/sin.(-PI/2) by Lm7,Th3,RFUNCT_1:def 2
.= 1/(-1) by SIN_COS:30,76
.= -1;
cosec.(-PI/4) = 1/(-1/sqrt 2) by Lm7,Th3,Th30,RFUNCT_1:def 2
.= -1/(1/sqrt 2) by XCMPLX_1:188
.= -sqrt 2;
hence thesis by A3,A2,A1;
end;
theorem Th33:
for x be set st x in [.0,PI/4.] holds sec.x in [.1,sqrt 2.]
proof
let x be set;
assume x in [.0,PI/4.];
then x in ].0,PI/4.[ \/ {0,PI/4} by XXREAL_1:128;
then
A1: x in ].0,PI/4.[ or x in {0,PI/4} by XBOOLE_0:def 3;
per cases by A1,TARSKI:def 2;
suppose
A2: x in ].0,PI/4.[;
PI/4 < PI/2 by XREAL_1:76;
then 0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[;
then
A3: [.0,PI/4.] c= [.0,PI/2.[ by XXREAL_2:def 12;
then
A4: sec|[.0,PI/4.] is increasing by Th17,RFUNCT_2:28;
A5: ex s be Real st s=x & 0 < s & s < PI/4 by A2;
A6: ].0,PI/4.[ c= [.0,PI/4.] by XXREAL_1:25;
A7: [.0,PI/4.] /\ dom sec = [.0,PI/4.] by A3,Th1,XBOOLE_1:1,28;
0 in [.0,PI/4.] & ex s be Real st s=x & 0 < s & s < PI/4 by A2;
then
A8: 1 < sec.x by A2,A4,A7,A6,Th31,RFUNCT_2:20;
PI/4 in [.0,PI/4.] /\ dom sec by A7;
then sec.x < sqrt 2 by A2,A4,A7,A6,A5,Th31,RFUNCT_2:20;
hence thesis by A8;
end;
suppose
x = 0;
hence thesis by Th31,SQUARE_1:19;
end;
suppose
x = PI/4;
hence thesis by Th31,SQUARE_1:19;
end;
end;
theorem Th34:
for x be set st x in [.3/4*PI,PI.] holds sec.x in [.-sqrt 2,-1.]
proof
let x be set;
A1: PI/4 < PI/2 by XREAL_1:76;
then
A2: PI/4+PI/2 < PI/2+PI/2 by XREAL_1:8;
assume x in [.3/4*PI,PI.];
then x in ].3/4*PI,PI.[ \/ {3/4*PI,PI} by A2,XXREAL_1:128;
then
A3: x in ].3/4*PI,PI.[ or x in {3/4*PI,PI} by XBOOLE_0:def 3;
per cases by A3,TARSKI:def 2;
suppose
A4: x in ].3/4*PI,PI.[;
PI/4+PI/4 < PI/2+PI/4 by A1,XREAL_1:8;
then
A5: 3/4*PI in ].PI/2,PI.] by A2;
PI in ].PI/2,PI.] by COMPTRIG:5;
then
A6: [.3/4*PI,PI.] c= ].PI/2,PI.] by A5,XXREAL_2:def 12;
then
A7: sec|[.3/4*PI,PI.] is increasing by Th18,RFUNCT_2:28;
A8: ex s be Real st s=x & 3/4*PI < s & s < PI by A4;
A9: ex s be Real st s=x & 3/4*PI < s & s < PI by A4;
A10: ].3/4*PI,PI.[ c= [.3/4*PI,PI.] by XXREAL_1:25;
A11: [.3/4*PI,PI.] /\ dom sec = [.3/4*PI,PI.] by A6,Th2,XBOOLE_1:1,28;
then PI in [.3/4*PI,PI.] /\ dom sec by A2;
then
A12: sec.x < -1 by A4,A7,A11,A10,A9,Th31,RFUNCT_2:20;
3/4*PI in [.3/4*PI,PI.] by A2;
then -sqrt 2 < sec.x by A4,A7,A11,A10,A8,Th31,RFUNCT_2:20;
hence thesis by A12;
end;
suppose
A13: x = 3/4*PI;
-sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
hence thesis by A13,Th31;
end;
suppose
A14: x = PI;
-sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
hence thesis by A14,Th31;
end;
end;
theorem Th35:
for x be set st x in [.-PI/2,-PI/4.] holds cosec.x in [.-sqrt 2, -1.]
proof
let x be set;
PI/4 < PI/2 by XREAL_1:76;
then
A1: -PI/2 < -PI/4 by XREAL_1:24;
assume x in [.-PI/2,-PI/4.];
then x in ].-PI/2,-PI/4.[ \/ {-PI/2,-PI/4} by A1,XXREAL_1:128;
then
A2: x in ].-PI/2,-PI/4.[ or x in {-PI/2,-PI/4} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 2;
suppose
A3: x in ].-PI/2,-PI/4.[;
then
A4: ex s be Real st s=x & -PI/2 < s & s < -PI/4;
A5: ex s be Real st s=x & -PI/2 < s & s < -PI/4 by A3;
A6: ].-PI/2,-PI/4.[ c= [.-PI/2,-PI/4.] by XXREAL_1:25;
-PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[ by A1;
then
A7: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by XXREAL_2:def 12;
then
A8: cosec|[.-PI/2,-PI/4.] is decreasing by Th19,RFUNCT_2:29;
A9: [.-PI/2,-PI/4.] /\ dom cosec = [.-PI/2,-PI/4.] by A7,Th3,XBOOLE_1:1,28;
then -PI/4 in [.-PI/2,-PI/4.] /\ dom cosec by A1;
then
A10: cosec.x > -sqrt 2 by A3,A8,A9,A6,A5,Th32,RFUNCT_2:21;
-PI/2 in [.-PI/2,-PI/4.] by A1;
then -1 > cosec.x by A3,A8,A9,A6,A4,Th32,RFUNCT_2:21;
hence thesis by A10;
end;
suppose
A11: x = -PI/2;
-sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
hence thesis by A11,Th32;
end;
suppose
A12: x = -PI/4;
-sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
hence thesis by A12,Th32;
end;
end;
theorem Th36:
for x be set st x in [.PI/4,PI/2.] holds cosec.x in [.1,sqrt 2.]
proof
let x be set;
A1: PI/4 < PI/2 by XREAL_1:76;
assume x in [.PI/4,PI/2.];
then x in ].PI/4,PI/2.[ \/ {PI/4,PI/2} by A1,XXREAL_1:128;
then
A2: x in ].PI/4,PI/2.[ or x in {PI/4,PI/2} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 2;
suppose
A3: x in ].PI/4,PI/2.[;
then
A4: ex s be Real st s=x & PI/4 < s & s < PI/2;
A5: ex s be Real st s=x & PI/4 < s & s < PI/2 by A3;
A6: ].PI/4,PI/2.[ c= [.PI/4,PI/2.] by XXREAL_1:25;
PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.] by A1;
then
A7: [.PI/4,PI/2.] c= ].0,PI/2.] by XXREAL_2:def 12;
then
A8: cosec|[.PI/4,PI/2.] is decreasing by Th20,RFUNCT_2:29;
A9: [.PI/4,PI/2.] /\ dom cosec = [.PI/4,PI/2.] by A7,Th4,XBOOLE_1:1,28;
then PI/2 in [.PI/4,PI/2.] /\ dom cosec by A1;
then
A10: cosec.x > 1 by A3,A8,A9,A6,A5,Th32,RFUNCT_2:21;
PI/4 in [.PI/4,PI/2.] by A1;
then sqrt 2 > cosec.x by A3,A8,A9,A6,A4,Th32,RFUNCT_2:21;
hence thesis by A10;
end;
suppose
x = PI/4;
hence thesis by Th32,SQUARE_1:19;
end;
suppose
x = PI/2;
hence thesis by Th32,SQUARE_1:19;
end;
end;
Lm29: dom (sec | [.0,PI/4.]) = [.0,PI/4.]
proof
[.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
hence thesis by Th1,RELAT_1:62,XBOOLE_1:1;
end;
Lm30: dom (sec | [.3/4*PI,PI.]) = [.3/4*PI,PI.]
proof
[.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
hence thesis by Th2,RELAT_1:62,XBOOLE_1:1;
end;
Lm31: dom (cosec | [.-PI/2,-PI/4.]) = [.-PI/2,-PI/4.]
proof
[.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
hence thesis by Th3,RELAT_1:62,XBOOLE_1:1;
end;
Lm32: dom (cosec | [.PI/4,PI/2.]) = [.PI/4,PI/2.]
proof
[.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
hence thesis by Th4,RELAT_1:62,XBOOLE_1:1;
end;
Lm33: dom (sec|[.0,PI/2.[) = [.0,PI/2.[ & for th st th in [.0,PI/2.[ holds (
sec|[.0,PI/2.[).th = sec.th
proof
dom (sec|[.0,PI/2.[) = dom sec /\ [.0,PI/2.[ by RELAT_1:61;
then dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,XBOOLE_1:28;
hence thesis by FUNCT_1:47;
end;
Lm34: dom (sec|].PI/2,PI.]) = ].PI/2,PI.] & for th st th in ].PI/2,PI.] holds
(sec|].PI/2,PI.]).th = sec.th
proof
dom (sec|].PI/2,PI.]) = dom sec /\ ].PI/2,PI.] by RELAT_1:61;
then dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,XBOOLE_1:28;
hence thesis by FUNCT_1:47;
end;
Lm35: dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ & for th st th in [.-PI/2,0.[
holds (cosec|[.-PI/2,0.[).th = cosec.th
proof
dom (cosec|[.-PI/2,0.[) = dom cosec /\ [.-PI/2,0.[ by RELAT_1:61;
then dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,XBOOLE_1:28;
hence thesis by FUNCT_1:47;
end;
Lm36: dom (cosec|].0,PI/2.]) = ].0,PI/2.] & for th st th in ].0,PI/2.] holds (
cosec|].0,PI/2.]).th = cosec.th
proof
dom (cosec|].0,PI/2.]) = dom cosec /\ ].0,PI/2.] by RELAT_1:61;
then dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,XBOOLE_1:28;
hence thesis by FUNCT_1:47;
end;
theorem Th37:
sec|[.0,PI/2.[ is continuous
proof
for th be Real st th in dom(sec|[.0,PI/2.[) holds sec|[.0,PI/2.[
is_continuous_in th
proof
let th be Real;
A1: cos is_differentiable_in th by SIN_COS:63;
assume
A2: th in dom(sec|[.0,PI/2.[);
then th in [.0,PI/2.[ by RELAT_1:57;
then cos.th <> 0 by Lm1,COMPTRIG:11;
then
A3: sec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
now
let rseq;
assume that
A4: rng rseq c= dom (sec|[.0,PI/2.[) and
A5: rseq is convergent & lim rseq = th;
A6: dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
now
let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:1;
then rseq.n in rng rseq by FUNCT_1:def 3;
then
A7: (sec|[.0,PI/2.[).(rseq.n) = sec.(rseq.n) by A4,A6,FUNCT_1:49;
(sec|[.0,PI/2.[).(rseq.n) = ((sec|[.0,PI/2.[)/*rseq).n by A4,
FUNCT_2:108;
hence ((sec|[.0,PI/2.[)/*rseq).n = (sec/*rseq).n by A4,A6,A7,Th1,
FUNCT_2:108,XBOOLE_1:1;
end;
then
A8: (sec|[.0,PI/2.[)/*rseq = sec/*rseq by FUNCT_2:63;
A9: rng rseq c= dom sec by A4,A6,Th1;
then sec.th = lim(sec/*rseq) by A3,A5,FCONT_1:def 1;
hence (sec|[.0,PI/2.[)/*rseq is convergent & (sec|[.0,PI/2.[).th = lim((
sec|[.0,PI/2.[)/*rseq) by A2,A3,A5,A9,A8,Lm33,FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th38:
sec|].PI/2,PI.] is continuous
proof
for th be Real st th in dom(sec|].PI/2,PI.]) holds sec|].PI/2,PI
.] is_continuous_in th
proof
let th be Real;
A1: cos is_differentiable_in th by SIN_COS:63;
assume
A2: th in dom(sec|].PI/2,PI.]);
then th in ].PI/2,PI.] by RELAT_1:57;
then cos.th <> 0 by Lm2,COMPTRIG:13;
then
A3: sec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
now
let rseq;
assume that
A4: rng rseq c= dom (sec|].PI/2,PI.]) and
A5: rseq is convergent & lim rseq = th;
A6: dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
now
let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:1;
then rseq.n in rng rseq by FUNCT_1:def 3;
then
A7: (sec|].PI/2,PI.]).(rseq.n) = sec.(rseq.n) by A4,A6,FUNCT_1:49;
(sec|].PI/2,PI.]).(rseq.n) = ((sec|].PI/2,PI.])/*rseq).n by A4,
FUNCT_2:108;
hence ((sec|].PI/2,PI.])/*rseq).n = (sec/*rseq).n by A4,A6,A7,Th2,
FUNCT_2:108,XBOOLE_1:1;
end;
then
A8: (sec|].PI/2,PI.])/*rseq = sec/*rseq by FUNCT_2:63;
A9: rng rseq c= dom sec by A4,A6,Th2;
then sec.th = lim(sec/*rseq) by A3,A5,FCONT_1:def 1;
hence
(sec|].PI/2,PI.])/*rseq is convergent & (sec|].PI/2,PI.]).th = lim(
(sec|].PI/2,PI.])/*rseq) by A2,A3,A5,A9,A8,Lm34,FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th39:
cosec|[.-PI/2,0.[ is continuous
proof
for th be Real st th in dom(cosec|[.-PI/2,0.[) holds cosec|[.-PI/
2,0.[ is_continuous_in th
proof
let th be Real;
assume
A1: th in dom(cosec|[.-PI/2,0.[);
then
A2: th in [.-PI/2,0.[ by RELAT_1:57;
then th < 0 by Lm3,XXREAL_1:4;
then
A3: th+2*PI < 0+2*PI by XREAL_1:8;
-PI < th by A2,Lm3,XXREAL_1:4;
then -PI+2*PI < th+2*PI by XREAL_1:8;
then th+2*PI in ].PI,2*PI.[ by A3;
then sin.(th+2*PI) <> 0 by COMPTRIG:9;
then
A4: sin.th <> 0 by SIN_COS:78;
sin is_differentiable_in th by SIN_COS:64;
then
A5: cosec is_continuous_in th by A4,FCONT_1:10,FDIFF_1:24;
now
let rseq;
assume that
A6: rng rseq c= dom (cosec|[.-PI/2,0.[) and
A7: rseq is convergent & lim rseq = th;
A8: dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
now
let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:1;
then rseq.n in rng rseq by FUNCT_1:def 3;
then
A9: (cosec|[.-PI/2,0.[).(rseq.n) = cosec.(rseq.n) by A6,A8,FUNCT_1:49;
(cosec|[.-PI/2,0.[).(rseq.n) = ((cosec|[.-PI/2,0.[)/*rseq).n by A6,
FUNCT_2:108;
hence ((cosec|[.-PI/2,0.[)/*rseq).n = (cosec/*rseq).n by A6,A8,A9,Th3,
FUNCT_2:108,XBOOLE_1:1;
end;
then
A10: (cosec|[.-PI/2,0.[)/*rseq = cosec/*rseq by FUNCT_2:63;
A11: rng rseq c= dom cosec by A6,A8,Th3;
then cosec.th = lim(cosec/*rseq) by A5,A7,FCONT_1:def 1;
hence (cosec|[.-PI/2,0.[)/*rseq is convergent & (cosec|[.-PI/2,0.[).th =
lim((cosec|[.-PI/2,0.[)/*rseq) by A1,A5,A7,A11,A10,Lm35,FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th40:
cosec|].0,PI/2.] is continuous
proof
for th be Real st th in dom(cosec|].0,PI/2.])holds cosec|].0,PI/2
.] is_continuous_in th
proof
let th be Real;
A1: sin is_differentiable_in th by SIN_COS:64;
assume
A2: th in dom(cosec|].0,PI/2.]);
then th in ].0,PI/2.] by RELAT_1:57;
then sin.th <> 0 by Lm4,COMPTRIG:7;
then
A3: cosec is_continuous_in th by A1,FCONT_1:10,FDIFF_1:24;
now
let rseq;
assume that
A4: rng rseq c= dom (cosec|].0,PI/2.]) and
A5: rseq is convergent & lim rseq = th;
A6: dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
now
let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:1;
then rseq.n in rng rseq by FUNCT_1:def 3;
then
A7: (cosec|].0,PI/2.]).(rseq.n) = cosec.(rseq.n) by A4,A6,FUNCT_1:49;
(cosec|].0,PI/2.]).(rseq.n) = ((cosec|].0,PI/2.])/*rseq).n by A4,
FUNCT_2:108;
hence ((cosec|].0,PI/2.])/*rseq).n = (cosec/*rseq).n by A4,A6,A7,Th4,
FUNCT_2:108,XBOOLE_1:1;
end;
then
A8: (cosec|].0,PI/2.])/*rseq = cosec/*rseq by FUNCT_2:63;
A9: rng rseq c= dom cosec by A4,A6,Th4;
then cosec.th = lim(cosec/*rseq) by A3,A5,FCONT_1:def 1;
hence (cosec|].0,PI/2.])/*rseq is convergent & (cosec|].0,PI/2.]).th =
lim((cosec|].0,PI/2.])/*rseq) by A2,A3,A5,A9,A8,Lm36,FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 1;
end;
hence thesis by FCONT_1:def 2;
end;
theorem Th41:
rng(sec | [.0,PI/4.]) = [.1,sqrt 2.]
proof
now
let y be object;
thus y in [.1,sqrt 2.] implies
ex x be object st x in dom (sec | [.0,PI/4.])
& y = (sec | [.0,PI/4.]).x
proof
assume
A1: y in [.1,sqrt 2.];
then reconsider y1=y as Real;
[.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
then
A2: sec|[.0,PI/4.] is continuous by Th37,FCONT_1:16;
y1 in [.sec.0,sec.(PI/4).] \/ [.sec.(PI/4),sec.0.] by A1,Th31,
XBOOLE_0:def 3;
then consider x be Real such that
A3: x in [.0,PI/4.] & y1 = sec.x by A2,Lm13,Th1,FCONT_2:15,XBOOLE_1:1;
take x;
thus thesis by A3,Lm29,FUNCT_1:49;
end;
thus (ex x be object
st x in dom (sec | [.0,PI/4.]) & y = (sec | [.0,PI/4.]).
x) implies y in [.1,sqrt 2.]
proof
given x be object such that
A4: x in dom (sec | [.0,PI/4.]) and
A5: y = (sec | [.0,PI/4.]).x;
reconsider x1=x as Real by A4;
y = sec.x1 by A4,A5,Lm29,FUNCT_1:49;
hence thesis by A4,Lm29,Th33;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th42:
rng(sec | [.3/4*PI,PI.]) = [.-sqrt 2,-1.]
proof
now
let y be object;
thus y in [.-sqrt 2,-1.] implies
ex x be object st x in dom (sec | [.3/4*PI,
PI.]) & y = (sec | [.3/4*PI,PI.]).x
proof
[.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
then
A1: sec|[.3/4*PI,PI.] is continuous by Th38,FCONT_1:16;
assume
A2: y in [.-sqrt 2,-1.];
then reconsider y1=y as Real;
A3: 3/4*PI <= PI by Lm6,XXREAL_1:2;
y1 in [.sec.(3/4*PI),sec.PI.] \/ [.sec.PI,sec.(3/4*PI).] by A2,Th31,
XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.3/4*PI,PI.] & y1 = sec.x by A3,A1,Lm14,Th2,FCONT_2:15,XBOOLE_1:1;
take x;
thus thesis by A4,Lm30,FUNCT_1:49;
end;
thus (ex x be object
st x in dom (sec | [.3/4*PI,PI.]) & y = (sec | [.3/4*PI,
PI.]).x) implies y in [.-sqrt 2,-1.]
proof
given x be object such that
A5: x in dom (sec | [.3/4*PI,PI.]) and
A6: y = (sec | [.3/4*PI,PI.]).x;
reconsider x1=x as Real by A5;
y = sec.x1 by A5,A6,Lm30,FUNCT_1:49;
hence thesis by A5,Lm30,Th34;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th43:
rng(cosec | [.-PI/2,-PI/4.]) = [.-sqrt 2,-1.]
proof
now
let y be object;
thus y in [.-sqrt 2,-1.] implies
ex x be object st x in dom (cosec | [.-PI/2,
-PI/4.]) & y = (cosec | [.-PI/2,-PI/4.]).x
proof
[.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
then
A1: cosec|[.-PI/2,-PI/4.] is continuous by Th39,FCONT_1:16;
assume
A2: y in [.-sqrt 2,-1.];
then reconsider y1=y as Real;
A3: -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
y1 in [.cosec.(-PI/4),cosec.(-PI/2).] \/ [.cosec.(-PI/2),cosec.(-PI/
4).] by A2,Th32,XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.-PI/2,-PI/4.] & y1 = cosec.x by A3,A1,Lm19,Th3,FCONT_2:15
,XBOOLE_1:1;
take x;
thus thesis by A4,Lm31,FUNCT_1:49;
end;
thus (ex x be object
st x in dom (cosec | [.-PI/2,-PI/4.]) & y = (cosec | [.-
PI/2,-PI/4.]).x) implies y in [.-sqrt 2,-1.]
proof
given x be object such that
A5: x in dom (cosec | [.-PI/2,-PI/4.]) and
A6: y = (cosec | [.-PI/2,-PI/4.]).x;
reconsider x1=x as Real by A5;
y = cosec.x1 by A5,A6,Lm31,FUNCT_1:49;
hence thesis by A5,Lm31,Th35;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th44:
rng(cosec | [.PI/4,PI/2.]) = [.1,sqrt 2.]
proof
now
let y be object;
thus y in [.1,sqrt 2.] implies
ex x be object st x in dom (cosec | [.PI/4,PI/
2.]) & y = (cosec | [.PI/4,PI/2.]).x
proof
[.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
then
A1: cosec|[.PI/4,PI/2.] is continuous by Th40,FCONT_1:16;
assume
A2: y in [.1,sqrt 2.];
then reconsider y1=y as Real;
A3: PI/4 <= PI/2 by Lm8,XXREAL_1:2;
y1 in [.cosec.(PI/2),cosec.(PI/4).] \/ [.cosec.(PI/4),cosec.(PI/2).]
by A2,Th32,XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.PI/4,PI/2.] & y1 = cosec.x by A3,A1,Lm20,Th4,FCONT_2:15,XBOOLE_1:1
;
take x;
thus thesis by A4,Lm32,FUNCT_1:49;
end;
thus (ex x be object
st x in dom (cosec | [.PI/4,PI/2.]) & y = (cosec | [.PI/
4,PI/2.]).x) implies y in [.1,sqrt 2.]
proof
given x be object such that
A5: x in dom (cosec | [.PI/4,PI/2.]) and
A6: y = (cosec | [.PI/4,PI/2.]).x;
reconsider x1=x as Real by A5;
y = cosec.x1 by A5,A6,Lm32,FUNCT_1:49;
hence thesis by A5,Lm32,Th36;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th45:
[.1,sqrt 2.] c= dom arcsec1
proof
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
rng(sec | [.0,PI/4.]) c= rng(sec | [.0,PI/2.[)
proof
let y be object;
assume y in rng(sec | [.0,PI/4.]);
then y in sec.:[.0,PI/4.] by RELAT_1:115;
then ex x be object st x in dom sec & x in [.0,PI/4.] & y = sec .x by
FUNCT_1:def 6;
then y in sec.:[.0,PI/2.[ by A1,FUNCT_1:def 6;
hence thesis by RELAT_1:115;
end;
hence thesis by Th41,FUNCT_1:33;
end;
theorem Th46:
[.-sqrt 2,-1.] c= dom arcsec2
proof
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
rng(sec | [.3/4*PI,PI.]) c= rng(sec | ].PI/2,PI.])
proof
let y be object;
assume y in rng(sec | [.3/4*PI,PI.]);
then y in sec.:[.3/4*PI,PI.] by RELAT_1:115;
then ex x be object st x in dom sec & x in [.3/4*PI,PI.] & y = sec.x by
FUNCT_1:def 6;
then y in sec.:].PI/2,PI.] by A1,FUNCT_1:def 6;
hence thesis by RELAT_1:115;
end;
hence thesis by Th42,FUNCT_1:33;
end;
theorem Th47:
[.-sqrt 2,-1.] c= dom arccosec1
proof
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
rng(cosec | [.-PI/2,-PI/4.]) c= rng(cosec | [.-PI/2,0.[)
proof
let y be object;
assume y in rng(cosec | [.-PI/2,-PI/4.]);
then y in cosec.:[.-PI/2,-PI/4.] by RELAT_1:115;
then ex x be object
st x in dom cosec & x in [.-PI/2,-PI/4.] & y = cosec.x by
FUNCT_1:def 6;
then y in cosec.:[.-PI/2,0.[ by A1,FUNCT_1:def 6;
hence thesis by RELAT_1:115;
end;
hence thesis by Th43,FUNCT_1:33;
end;
theorem Th48:
[.1,sqrt 2.] c= dom arccosec2
proof
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
rng(cosec | [.PI/4,PI/2.]) c= rng(cosec | ].0,PI/2.])
proof
let y be object;
assume y in rng(cosec | [.PI/4,PI/2.]);
then y in cosec.:[.PI/4,PI/2.] by RELAT_1:115;
then ex x be object
st x in dom cosec & x in [.PI/4,PI/2.] & y = cosec.x by
FUNCT_1:def 6;
then y in cosec.:].0,PI/2.] by A1,FUNCT_1:def 6;
hence thesis by RELAT_1:115;
end;
hence thesis by Th44,FUNCT_1:33;
end;
Lm37: sec | [.0,PI/4.]|[.0,PI/4.] is increasing
proof
[.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
then sec|[.0,PI/4.] is increasing by Th17,RFUNCT_2:28;
hence thesis;
end;
Lm38: sec | [.3/4*PI,PI.]|[.3/4*PI,PI.] is increasing
proof
[.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
then sec|[.3/4*PI,PI.] is increasing by Th18,RFUNCT_2:28;
hence thesis;
end;
Lm39: cosec | [.-PI/2,-PI/4.] |[.-PI/2,-PI/4.] is decreasing
proof
[.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
then cosec|[.-PI/2,-PI/4.] is decreasing by Th19,RFUNCT_2:29;
hence thesis;
end;
Lm40: cosec | [.PI/4,PI/2.]|[.PI/4,PI/2.] is decreasing
proof
[.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
then cosec|[.PI/4,PI/2.] is decreasing by Th20,RFUNCT_2:29;
hence thesis;
end;
Lm41: sec | [.0,PI/4.] is one-to-one
proof
[.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
then (sec | [.0,PI/2.[) | [.0,PI/4.] = sec | [.0,PI/4.] by RELAT_1:74;
hence thesis;
end;
Lm42: sec | [.3/4*PI,PI.] is one-to-one
proof
[.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
then (sec | ].PI/2,PI.]) | [.3/4*PI,PI.] = sec | [.3/4*PI,PI.] by RELAT_1:74;
hence thesis;
end;
Lm43: cosec | [.-PI/2,-PI/4.] is one-to-one
proof
[.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
then (cosec | [.-PI/2,0.[) | [.-PI/2,-PI/4.] = cosec | [.-PI/2,-PI/4.] by
RELAT_1:74;
hence thesis;
end;
Lm44: cosec | [.PI/4,PI/2.] is one-to-one
proof
[.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
then (cosec | ].0,PI/2.]) | [.PI/4,PI/2.] = cosec | [.PI/4,PI/2.] by
RELAT_1:74;
hence thesis;
end;
registration
cluster sec | [.0,PI/4.] -> one-to-one;
coherence by Lm41;
cluster sec | [.3/4*PI,PI.] -> one-to-one;
coherence by Lm42;
cluster cosec | [.-PI/2,-PI/4.] -> one-to-one;
coherence by Lm43;
cluster cosec | [.PI/4,PI/2.] -> one-to-one;
coherence by Lm44;
end;
theorem Th49:
arcsec1 | [.1,sqrt 2.] = (sec | [.0,PI/4.])"
proof
set h = sec | [.0,PI/2.[;
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm5,XXREAL_2:def 12;
then (sec | [.0,PI/4.])" = (h | [.0,PI/4.])" by RELAT_1:74
.= h" | (h.:[.0,PI/4.]) by RFUNCT_2:17
.= h" | rng (h | [.0,PI/4.]) by RELAT_1:115
.= h" | ([.1,sqrt 2.]) by A1,Th41,RELAT_1:74;
hence thesis;
end;
theorem Th50:
arcsec2 | [.-sqrt 2,-1.] = (sec | [.3/4*PI,PI.])"
proof
set h = sec | ].PI/2,PI.];
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6,XXREAL_2:def 12;
then (sec | [.3/4*PI,PI.])" = (h | [.3/4*PI,PI.])" by RELAT_1:74
.= h" | (h.:[.3/4*PI,PI.]) by RFUNCT_2:17
.= h" | rng (h | [.3/4*PI,PI.]) by RELAT_1:115
.= h" | ([.-sqrt 2,-1.]) by A1,Th42,RELAT_1:74;
hence thesis;
end;
theorem Th51:
arccosec1 | [.-sqrt 2,-1.] = (cosec | [.-PI/2,-PI/4.])"
proof
set h = cosec | [.-PI/2,0.[;
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm7,XXREAL_2:def 12;
then (cosec | [.-PI/2,-PI/4.])" = (h | [.-PI/2,-PI/4.])" by RELAT_1:74
.= h" | (h.:[.-PI/2,-PI/4.]) by RFUNCT_2:17
.= h" | rng (h | [.-PI/2,-PI/4.]) by RELAT_1:115
.= h" | ([.-sqrt 2,-1.]) by A1,Th43,RELAT_1:74;
hence thesis;
end;
theorem Th52:
arccosec2 | [.1,sqrt 2.] = (cosec | [.PI/4,PI/2.])"
proof
set h = cosec | ].0,PI/2.];
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,XXREAL_2:def 12;
then (cosec | [.PI/4,PI/2.])" = (h | [.PI/4,PI/2.])" by RELAT_1:74
.= h" | (h.:[.PI/4,PI/2.]) by RFUNCT_2:17
.= h" | rng (h | [.PI/4,PI/2.]) by RELAT_1:115
.= h" | ([.1,sqrt 2.]) by A1,Th44,RELAT_1:74;
hence thesis;
end;
theorem
(sec | [.0,PI/4.]) qua Function * (arcsec1 | [.1,sqrt 2.]) = id [.1,
sqrt 2.] by Th41,Th49,FUNCT_1:39;
theorem
(sec | [.3/4*PI,PI.]) qua Function * (arcsec2 | [.-sqrt 2,-1.]) = id
[.-sqrt 2,-1.] by Th42,Th50,FUNCT_1:39;
theorem
(cosec | [.-PI/2,-PI/4.]) qua Function * (arccosec1 | [.-sqrt 2,-1.])
= id [.-sqrt 2,-1.] by Th43,Th51,FUNCT_1:39;
theorem
(cosec | [.PI/4,PI/2.]) qua Function * (arccosec2 | [.1,sqrt 2.]) = id
[.1,sqrt 2.] by Th44,Th52,FUNCT_1:39;
theorem
(sec | [.0,PI/4.]) * (arcsec1 | [.1,sqrt 2.]) = id [.1,sqrt 2.] by Th41,Th49,
FUNCT_1:39;
theorem
(sec | [.3/4*PI,PI.]) * (arcsec2 | [.-sqrt 2,-1.]) = id [.-sqrt 2,-1.]
by Th42,Th50,FUNCT_1:39;
theorem
(cosec | [.-PI/2,-PI/4.]) * (arccosec1 | [.-sqrt 2,-1.]) = id [.-sqrt
2,-1.] by Th43,Th51,FUNCT_1:39;
theorem
(cosec | [.PI/4,PI/2.]) * (arccosec2 | [.1,sqrt 2.]) = id [.1,sqrt 2.]
by Th44,Th52,FUNCT_1:39;
theorem
arcsec1 qua Function * (sec | [.0,PI/2.[) = id [.0,PI/2.[ by Lm25,Th25,
FUNCT_1:39;
theorem
arcsec2 qua Function * (sec | ].PI/2,PI.]) = id ].PI/2,PI.] by Lm26,Th26,
FUNCT_1:39;
theorem
arccosec1 qua Function * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[ by Lm27,Th27,
FUNCT_1:39;
theorem
arccosec2 qua Function * (cosec | ].0,PI/2.]) = id ].0,PI/2.] by Lm28,Th28,
FUNCT_1:39;
theorem Th65:
arcsec1 * (sec | [.0,PI/2.[) = id [.0,PI/2.[ by Lm25,Th25,FUNCT_1:39;
theorem Th66:
arcsec2 * (sec | ].PI/2,PI.]) = id ].PI/2,PI.] by Lm26,Th26,FUNCT_1:39;
theorem Th67:
arccosec1 * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[ by Lm27,Th27,FUNCT_1:39;
theorem Th68:
arccosec2 * (cosec | ].0,PI/2.]) = id ].0,PI/2.] by Lm28,Th28,FUNCT_1:39;
theorem Th69:
0 <= r & r < PI/2 implies arcsec1 sec.r = r
proof
A1: dom (sec | [.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:62;
assume 0 <= r & r < PI/2;
then
A2: r in [.0,PI/2.[;
then arcsec1 sec.r = arcsec1.((sec|[.0,PI/2.[).r) by FUNCT_1:49
.= (id [.0,PI/2.[).r by A2,A1,Th65,FUNCT_1:13
.= r by A2,FUNCT_1:18;
hence thesis;
end;
theorem Th70:
PI/2 < r & r <= PI implies arcsec2 sec.r = r
proof
A1: dom (sec | ].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:62;
assume PI/2 < r & r <= PI;
then
A2: r in ].PI/2,PI.];
then arcsec2 sec.r = arcsec2.((sec|].PI/2,PI.]).r) by FUNCT_1:49
.= (id ].PI/2,PI.]).r by A2,A1,Th66,FUNCT_1:13
.= r by A2,FUNCT_1:18;
hence thesis;
end;
theorem Th71:
-PI/2 <= r & r < 0 implies arccosec1 cosec.r = r
proof
A1: dom (cosec | [.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:62;
assume -PI/2 <= r & r < 0;
then
A2: r in [.-PI/2,0.[;
then arccosec1 cosec.r = arccosec1.((cosec|[.-PI/2,0.[).r) by FUNCT_1:49
.= (id [.-PI/2,0.[).r by A2,A1,Th67,FUNCT_1:13
.= r by A2,FUNCT_1:18;
hence thesis;
end;
theorem Th72:
0 < r & r <= PI/2 implies arccosec2 cosec.r = r
proof
A1: dom (cosec | ].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:62;
assume 0 < r & r <= PI/2;
then
A2: r in ].0,PI/2.];
then arccosec2 cosec.r = arccosec2.((cosec|].0,PI/2.]).r) by FUNCT_1:49
.= (id ].0,PI/2.]).r by A2,A1,Th68,FUNCT_1:13
.= r by A2,FUNCT_1:18;
hence thesis;
end;
theorem Th73:
arcsec1.1 = 0 & arcsec1.(sqrt 2) = PI/4
proof
A1: arcsec1.1 = arcsec1 1 .= 0 by Th31,Th69;
A2: PI/4 < PI/2 by Lm5,XXREAL_1:3;
arcsec1.(sqrt 2) = arcsec1 (sqrt 2) .= PI/4 by A2,Th31,Th69;
hence thesis by A1;
end;
theorem Th74:
arcsec2.(-sqrt 2) = 3/4*PI & arcsec2.(-1) = PI
proof
A1: PI/2 < PI by Lm6,XXREAL_1:2;
A2: arcsec2.(-1) = arcsec2 (-1) .= PI by A1,Th31,Th70;
A3: PI/2 < 3/4*PI & 3/4*PI <= PI by Lm6,XXREAL_1:2;
arcsec2.(-sqrt 2) = arcsec2 (-sqrt 2) .= 3/4*PI by A3,Th31,Th70;
hence thesis by A2;
end;
theorem Th75:
arccosec1.(-1) = -PI/2 & arccosec1.(-sqrt 2) = -PI/4
proof
A1: arccosec1.(-1) = arccosec1 (-1) .= -PI/2 by Th32,Th71;
A2: -PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
arccosec1.(-sqrt 2) = arccosec1 (-sqrt 2) .= -PI/4 by A2,Th32,Th71;
hence thesis by A1;
end;
theorem Th76:
arccosec2.(sqrt 2) = PI/4 & arccosec2.1 = PI/2
proof
A1: arccosec2.1 = arccosec2 1 .= PI/2 by Th32,Th72;
A2: PI/4 <= PI/2 by Lm8,XXREAL_1:2;
arccosec2.(sqrt 2) = arccosec2 (sqrt 2) .= PI/4 by A2,Th32,Th72;
hence thesis by A1;
end;
theorem Th77:
arcsec1|(sec.:[.0,PI/2.[) is increasing
proof
set f = sec | [.0,PI/2.[;
A1: f.:[.0,PI/2.[ = rng(f|[.0,PI/2.[) by RELAT_1:115
.= rng(sec|[.0,PI/2.[) by RELAT_1:73
.= sec.:[.0,PI/2.[ by RELAT_1:115;
f|[.0,PI/2.[ = f by RELAT_1:73;
hence thesis by A1,Th17,FCONT_3:9;
end;
theorem Th78:
arcsec2|(sec.:].PI/2,PI.]) is increasing
proof
set f = sec | ].PI/2,PI.];
A1: f.:].PI/2,PI.] = rng(f|].PI/2,PI.]) by RELAT_1:115
.= rng(sec|].PI/2,PI.]) by RELAT_1:73
.= sec.:].PI/2,PI.] by RELAT_1:115;
f|].PI/2,PI.] = f by RELAT_1:73;
hence thesis by A1,Th18,FCONT_3:9;
end;
theorem Th79:
arccosec1|(cosec.:[.-PI/2,0.[) is decreasing
proof
set f = cosec | [.-PI/2,0.[;
A1: f.:[.-PI/2,0.[ = rng(f|[.-PI/2,0.[) by RELAT_1:115
.= rng(cosec|[.-PI/2,0.[) by RELAT_1:73
.= cosec.:[.-PI/2,0.[ by RELAT_1:115;
f|[.-PI/2,0.[ = f by RELAT_1:73;
hence thesis by A1,Th19,FCONT_3:10;
end;
theorem Th80:
arccosec2|(cosec.:].0,PI/2.]) is decreasing
proof
set f = cosec | ].0,PI/2.];
A1: f.:].0,PI/2.] = rng(f|].0,PI/2.]) by RELAT_1:115
.= rng(cosec|].0,PI/2.]) by RELAT_1:73
.= cosec.:].0,PI/2.] by RELAT_1:115;
f|].0,PI/2.] = f by RELAT_1:73;
hence thesis by A1,Th20,FCONT_3:10;
end;
theorem Th81:
arcsec1|[.1,sqrt 2.] is increasing
proof
[.1,sqrt 2.] = sec.:[.0,PI/4.] & [.0,PI/4.] c= [.0,PI/2.[ by Lm5,Th41,
RELAT_1:115,XXREAL_2:def 12;
hence thesis by Th77,RELAT_1:123,RFUNCT_2:28;
end;
theorem Th82:
arcsec2|[.-sqrt 2,-1.] is increasing
proof
[.-sqrt 2,-1.] = sec.:[.3/4*PI,PI.] & [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm6
,Th42,RELAT_1:115,XXREAL_2:def 12;
hence thesis by Th78,RELAT_1:123,RFUNCT_2:28;
end;
theorem Th83:
arccosec1|[.-sqrt 2,-1.] is decreasing
proof
[.-sqrt 2,-1.] = cosec.:[.-PI/2,-PI/4.] & [.-PI/2,-PI/4.] c= [.-PI/2,0.[
by Lm7,Th43,RELAT_1:115,XXREAL_2:def 12;
hence thesis by Th79,RELAT_1:123,RFUNCT_2:29;
end;
theorem Th84:
arccosec2|[.1,sqrt 2.] is decreasing
proof
[.1,sqrt 2.] = cosec.:[.PI/4,PI/2.] & [.PI/4,PI/2.] c= ].0,PI/2.] by Lm8,Th44
,RELAT_1:115,XXREAL_2:def 12;
hence thesis by Th80,RELAT_1:123,RFUNCT_2:29;
end;
theorem Th85:
for x be set st x in [.1,sqrt 2.] holds arcsec1.x in [.0,PI/4.]
proof
let x be set;
assume x in [.1,sqrt 2.];
then x in ].1,sqrt 2.[ \/ {1,sqrt 2} by SQUARE_1:19,XXREAL_1:128;
then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 3;
per cases by A1,TARSKI:def 2;
suppose
A2: x in ].1,sqrt 2.[;
then
A3: ].1,sqrt 2.[ c= [.1,sqrt 2.] &
ex s be Real st s=x & 1 < s & s < sqrt 2 by XXREAL_1:25;
A4: [.1,sqrt 2.] /\ dom arcsec1 = [.1,sqrt 2.] by Th45,XBOOLE_1:28;
then sqrt 2 in [.1,sqrt 2.] /\ dom arcsec1 by SQUARE_1:19;
then
A5: arcsec1.x < PI/4 by A2,A4,A3,Th73,Th81,RFUNCT_2:20;
1 in [.1,sqrt 2.] by SQUARE_1:19;
then 0 < arcsec1.x by A2,A4,A3,Th73,Th81,RFUNCT_2:20;
hence thesis by A5;
end;
suppose
x = 1;
hence thesis by Th73;
end;
suppose
x = sqrt 2;
hence thesis by Th73;
end;
end;
theorem Th86:
for x be set st x in [.-sqrt 2,-1.] holds arcsec2.x in [.3/4*PI, PI.]
proof
let x be set;
A1: -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
assume x in [.-sqrt 2,-1.];
then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1} by A1,XXREAL_1:128;
then
A2: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 2;
suppose
A3: x in ].-sqrt 2,-1.[;
then
A4: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] &
ex s be Real st s=x & -sqrt 2 < s &
s < - 1 by XXREAL_1:25;
A5: [.-sqrt 2,-1.] /\ dom arcsec2 = [.-sqrt 2,-1.] by Th46,XBOOLE_1:28;
then -1 in [.-sqrt 2,-1.] /\ dom arcsec2 by A1;
then
A6: arcsec2.x < PI by A3,A5,A4,Th74,Th82,RFUNCT_2:20;
-sqrt 2 in [.-sqrt 2,-1.] by A1;
then 3/4*PI < arcsec2.x by A3,A5,A4,Th74,Th82,RFUNCT_2:20;
hence thesis by A6;
end;
suppose
A7: x = -sqrt 2;
3/4*PI <= PI by Lm6,XXREAL_1:2;
hence thesis by A7,Th74;
end;
suppose
A8: x = -1;
3/4*PI <= PI by Lm6,XXREAL_1:2;
hence thesis by A8,Th74;
end;
end;
theorem Th87:
for x be set st x in [.-sqrt 2,-1.] holds arccosec1.x in [.-PI/2 ,-PI/4.]
proof
let x be set;
A1: -sqrt 2 < -1 by SQUARE_1:19,XREAL_1:24;
assume x in [.-sqrt 2,-1.];
then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1} by A1,XXREAL_1:128;
then
A2: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 3;
per cases by A2,TARSKI:def 2;
suppose
A3: x in ].-sqrt 2,-1.[;
then
A4: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] &
ex s be Real st s=x & -sqrt 2 < s &
s < - 1 by XXREAL_1:25;
A5: [.-sqrt 2,-1.] /\ dom arccosec1 = [.-sqrt 2,-1.] by Th47,XBOOLE_1:28;
then -1 in [.-sqrt 2,-1.] /\ dom arccosec1 by A1;
then
A6: arccosec1.x > -PI/2 by A3,A5,A4,Th75,Th83,RFUNCT_2:21;
-sqrt 2 in [.-sqrt 2,-1.] by A1;
then -PI/4 > arccosec1.x by A3,A5,A4,Th75,Th83,RFUNCT_2:21;
hence thesis by A6;
end;
suppose
A7: x = -sqrt 2;
-PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
hence thesis by A7,Th75;
end;
suppose
A8: x = -1;
-PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
hence thesis by A8,Th75;
end;
end;
theorem Th88:
for x be set st x in [.1,sqrt 2.] holds arccosec2.x in [.PI/4,PI /2.]
proof
let x be set;
assume x in [.1,sqrt 2.];
then x in ].1,sqrt 2.[ \/ {1,sqrt 2} by SQUARE_1:19,XXREAL_1:128;
then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 3;
per cases by A1,TARSKI:def 2;
suppose
A2: x in ].1,sqrt 2.[;
then
A3: ].1,sqrt 2.[ c= [.1,sqrt 2.] &
ex s be Real st s=x & 1 < s & s < sqrt
2 by XXREAL_1:25;
A4: [.1,sqrt 2.] /\ dom arccosec2 = [.1,sqrt 2.] by Th48,XBOOLE_1:28;
then sqrt 2 in [.1,sqrt 2.] /\ dom arccosec2 by SQUARE_1:19;
then
A5: arccosec2.x > PI/4 by A2,A4,A3,Th76,Th84,RFUNCT_2:21;
1 in [.1,sqrt 2.] by SQUARE_1:19;
then PI/2 > arccosec2.x by A2,A4,A3,Th76,Th84,RFUNCT_2:21;
hence thesis by A5;
end;
suppose
A6: x = 1;
PI/4 <= PI/2 by Lm8,XXREAL_1:2;
hence thesis by A6,Th76;
end;
suppose
A7: x = sqrt 2;
PI/4 <= PI/2 by Lm8,XXREAL_1:2;
hence thesis by A7,Th76;
end;
end;
theorem Th89:
1 <= r & r <= sqrt 2 implies sec.(arcsec1 r) = r
proof
assume 1 <= r & r <= sqrt 2;
then
A1: r in [.1,sqrt 2.];
then
A2: r in dom (arcsec1|[.1,sqrt 2.]) by Th45,RELAT_1:62;
sec.(arcsec1 r) = ((sec|[.0,PI/4.]) qua Function).(arcsec1.r) by A1,Th85,
FUNCT_1:49
.= ((sec|[.0,PI/4.]) qua Function).((arcsec1|[.1,sqrt 2.]).r) by A1,
FUNCT_1:49
.= ((sec|[.0,PI/4.]) qua Function * (arcsec1|[.1,sqrt 2.])).r by A2,
FUNCT_1:13
.= (id [.1,sqrt 2.]).r by Th41,Th49,FUNCT_1:39
.= r by A1,FUNCT_1:18;
hence thesis;
end;
theorem Th90:
-sqrt 2 <= r & r <= -1 implies sec.(arcsec2 r ) = r
proof
assume -sqrt 2 <= r & r <= -1;
then
A1: r in [.-sqrt 2,-1.];
then
A2: r in dom (arcsec2|[.-sqrt 2,-1.]) by Th46,RELAT_1:62;
sec.(arcsec2 r) = ((sec|[.3/4*PI,PI.]) qua Function).(arcsec2.r) by A1,Th86,
FUNCT_1:49
.= ((sec|[.3/4*PI,PI.]) qua Function).((arcsec2|[.-sqrt 2,-1.]).r) by A1,
FUNCT_1:49
.= ((sec|[.3/4*PI,PI.]) qua Function * (arcsec2|[.-sqrt 2,-1.])).r by A2,
FUNCT_1:13
.= (id [.-sqrt 2,-1.]).r by Th42,Th50,FUNCT_1:39
.= r by A1,FUNCT_1:18;
hence thesis;
end;
theorem Th91:
-sqrt 2 <= r & r <= -1 implies cosec.(arccosec1 r) = r
proof
assume -sqrt 2 <= r & r <= -1;
then
A1: r in [.-sqrt 2,-1.];
then
A2: r in dom (arccosec1|[.-sqrt 2,-1.]) by Th47,RELAT_1:62;
cosec.(arccosec1 r) = ((cosec|[.-PI/2,-PI/4.]) qua Function).(arccosec1.
r) by A1,Th87,FUNCT_1:49
.= ((cosec|[.-PI/2,-PI/4.]) qua Function).((arccosec1|[.-sqrt 2,-1.]).r)
by A1,FUNCT_1:49
.= ((cosec|[.-PI/2,-PI/4.]) qua Function * (arccosec1|[.-sqrt 2,-1.])).r
by A2,FUNCT_1:13
.= (id [.-sqrt 2,-1.]).r by Th43,Th51,FUNCT_1:39
.= r by A1,FUNCT_1:18;
hence thesis;
end;
theorem Th92:
1 <= r & r <= sqrt 2 implies cosec.(arccosec2 r) = r
proof
assume 1 <= r & r <= sqrt 2;
then
A1: r in [.1,sqrt 2.];
then
A2: r in dom (arccosec2|[.1,sqrt 2.]) by Th48,RELAT_1:62;
cosec.(arccosec2 r) = ((cosec|[.PI/4,PI/2.]) qua Function).(arccosec2.r)
by A1,Th88,FUNCT_1:49
.= ((cosec|[.PI/4,PI/2.]) qua Function).((arccosec2|[.1,sqrt 2.]).r) by A1,
FUNCT_1:49
.= ((cosec|[.PI/4,PI/2.]) qua Function * (arccosec2|[.1,sqrt 2.])).r by A2,
FUNCT_1:13
.= (id [.1,sqrt 2.]).r by Th44,Th52,FUNCT_1:39
.= r by A1,FUNCT_1:18;
hence thesis;
end;
theorem Th93:
arcsec1|[.1,sqrt 2.] is continuous
proof
set f = sec | [.0,PI/4.];
f|[.0,PI/4.] = f & (f|[.0,PI/4.])"|(f.:[.0,PI/4.]) is continuous by Lm29,Lm37
,FCONT_1:47,RELAT_1:72;
then arcsec1|[.1,sqrt 2.]|[.1,sqrt 2.] is continuous by Th41,Th49,RELAT_1:115
;
hence thesis by FCONT_1:15;
end;
theorem Th94:
arcsec2|[.-sqrt 2,-1.] is continuous
proof
set f = sec | [.3/4*PI,PI.];
3/4*PI <= PI by Lm6,XXREAL_1:2;
then f|[.3/4*PI,PI.] = f & (f|[.3/4*PI,PI.])"|(f.:[.3/4*PI,PI.]) is
continuous by Lm30,Lm38,FCONT_1:47,RELAT_1:72;
then arcsec2|[.-sqrt 2,-1.]|[.-sqrt 2,-1.] is continuous by Th42,Th50,
RELAT_1:115;
hence thesis by FCONT_1:15;
end;
theorem Th95:
arccosec1|[.-sqrt 2,-1.] is continuous
proof
set f = cosec | [.-PI/2,-PI/4.];
-PI/2 <= -PI/4 by Lm7,XXREAL_1:3;
then f|[.-PI/2,-PI/4.] = f & (f|[.-PI/2,-PI/4.])"|(f.:[.-PI/2,-PI/4.]) is
continuous by Lm31,Lm39,FCONT_1:47,RELAT_1:72;
then arccosec1|[.-sqrt 2,-1.]|[.-sqrt 2,-1.] is continuous by Th43,Th51,
RELAT_1:115;
hence thesis by FCONT_1:15;
end;
theorem Th96:
arccosec2|[.1,sqrt 2.] is continuous
proof
set f = cosec | [.PI/4,PI/2.];
PI/4 <= PI/2 by Lm8,XXREAL_1:2;
then f|[.PI/4,PI/2.] = f & (f|[.PI/4,PI/2.])"|(f.:[.PI/4,PI/2.]) is
continuous by Lm32,Lm40,FCONT_1:47,RELAT_1:72;
then arccosec2|[.1,sqrt 2.]|[.1,sqrt 2.] is continuous by Th44,Th52,
RELAT_1:115;
hence thesis by FCONT_1:15;
end;
theorem Th97:
rng(arcsec1 | [.1,sqrt 2.]) = [.0,PI/4.]
proof
now
let y be object;
thus y in [.0,PI/4.] implies
ex x be object st x in dom (arcsec1 | [.1,sqrt 2
.]) & y = (arcsec1 | [.1,sqrt 2.]).x
proof
assume
A1: y in [.0,PI/4.];
then reconsider y1=y as Real;
y1 in [.arcsec1.1,arcsec1.(sqrt 2).] \/ [.arcsec1.(sqrt 2),arcsec1.1
.] by A1,Th73,XBOOLE_0:def 3;
then consider x be Real such that
A2: x in [.1,sqrt 2.] & y1 = arcsec1.x by Th45,Th93,FCONT_2:15,SQUARE_1:19;
take x;
thus thesis by A2,Th45,FUNCT_1:49,RELAT_1:62;
end;
thus (ex x be object
st x in dom (arcsec1 | [.1,sqrt 2.]) & y = (arcsec1 | [.
1,sqrt 2.]).x) implies y in [.0,PI/4.]
proof
given x be object such that
A3: x in dom (arcsec1 | [.1,sqrt 2.]) and
A4: y = (arcsec1 | [.1,sqrt 2.]).x;
A5: dom (arcsec1 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th45,RELAT_1:62;
then y = arcsec1.x by A3,A4,FUNCT_1:49;
hence thesis by A3,A5,Th85;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th98:
rng(arcsec2 | [.-sqrt 2,-1.]) = [.3/4*PI,PI.]
proof
now
let y be object;
thus y in [.3/4*PI,PI.] implies
ex x be object st x in dom (arcsec2 | [.-sqrt
2,-1.]) & y = (arcsec2 | [.-sqrt 2,-1.]).x
proof
assume
A1: y in [.3/4*PI,PI.];
then reconsider y1=y as Real;
-sqrt 2 < -1 & y1 in [.arcsec2.(-sqrt 2),arcsec2.(-1).] \/ [.arcsec2
.(-1), arcsec2.(-sqrt 2).] by A1,Th74,SQUARE_1:19,XBOOLE_0:def 3,XREAL_1:24;
then consider x be Real such that
A2: x in [.-sqrt 2,-1.] & y1 = arcsec2.x by Th46,Th94,FCONT_2:15;
take x;
thus thesis by A2,Th46,FUNCT_1:49,RELAT_1:62;
end;
thus (ex x be object
st x in dom (arcsec2 | [.-sqrt 2,-1.]) & y = (arcsec2 |
[.-sqrt 2,-1.]).x) implies y in [.3/4*PI,PI.]
proof
given x be object such that
A3: x in dom (arcsec2 | [.-sqrt 2,-1.]) and
A4: y = (arcsec2 | [.-sqrt 2,-1.]).x;
A5: dom (arcsec2 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th46,RELAT_1:62;
then y = arcsec2.x by A3,A4,FUNCT_1:49;
hence thesis by A3,A5,Th86;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th99:
rng(arccosec1 | [.-sqrt 2,-1.]) = [.-PI/2,-PI/4.]
proof
now
let y be object;
thus y in [.-PI/2,-PI/4.] implies
ex x be object st x in dom (arccosec1 | [.-
sqrt 2,-1.]) & y = (arccosec1 | [.-sqrt 2,-1.]).x
proof
assume
A1: y in [.-PI/2,-PI/4.];
then reconsider y1=y as Real;
-sqrt 2 < -1 & y1 in [.arccosec1.(-1),arccosec1.(-sqrt 2).] \/ [.
arccosec1.( -sqrt 2),arccosec1.(-1).] by A1,Th75,SQUARE_1:19,XBOOLE_0:def 3
,XREAL_1:24;
then consider x be Real such that
A2: x in [.-sqrt 2,-1.] & y1 = arccosec1.x by Th47,Th95,FCONT_2:15;
take x;
thus thesis by A2,Th47,FUNCT_1:49,RELAT_1:62;
end;
thus (ex x be object st x in dom (arccosec1 | [.-sqrt 2,-1.]) & y = (
arccosec1 | [.-sqrt 2,-1.]).x) implies y in [.-PI/2,-PI/4.]
proof
given x be object such that
A3: x in dom (arccosec1 | [.-sqrt 2,-1.]) and
A4: y = (arccosec1 | [.-sqrt 2,-1.]).x;
A5: dom (arccosec1 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th47,RELAT_1:62;
then y = arccosec1.x by A3,A4,FUNCT_1:49;
hence thesis by A3,A5,Th87;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th100:
rng(arccosec2 | [.1,sqrt 2.]) = [.PI/4,PI/2.]
proof
now
let y be object;
thus y in [.PI/4,PI/2.] implies
ex x be object st x in dom (arccosec2 | [.1,
sqrt 2.]) & y = (arccosec2 | [.1,sqrt 2.]).x
proof
assume
A1: y in [.PI/4,PI/2.];
then reconsider y1=y as Real;
y1 in [.arccosec2.(sqrt 2),arccosec2.1.] \/ [.arccosec2.1,arccosec2.
(sqrt 2).] by A1,Th76,XBOOLE_0:def 3;
then consider x be Real such that
A2: x in [.1,sqrt 2.] & y1 = arccosec2.x by Th48,Th96,FCONT_2:15,SQUARE_1:19;
take x;
thus thesis by A2,Th48,FUNCT_1:49,RELAT_1:62;
end;
thus (ex x be object
st x in dom (arccosec2 | [.1,sqrt 2.]) & y = (arccosec2
| [.1,sqrt 2.]).x) implies y in [.PI/4,PI/2.]
proof
given x be object such that
A3: x in dom (arccosec2 | [.1,sqrt 2.]) and
A4: y = (arccosec2 | [.1,sqrt 2.]).x;
A5: dom (arccosec2 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th48,RELAT_1:62;
then y = arccosec2.x by A3,A4,FUNCT_1:49;
hence thesis by A3,A5,Th88;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem
(1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1) & (1 <= r & r <=
sqrt 2 & arcsec1 r = PI/4 implies r = sqrt 2) by Th31,Th89;
theorem
(-sqrt 2 <= r & r <= -1 & arcsec2 r = 3/4*PI implies r = -sqrt 2) & (-
sqrt 2 <= r & r <= -1 & arcsec2 r = PI implies r = -1) by Th31,Th90;
theorem
(-sqrt 2 <= r & r <= -1 & arccosec1 r = -PI/2 implies r = -1) & (-sqrt
2 <= r & r <= -1 & arccosec1 r = -PI/4 implies r = -sqrt 2) by Th32,Th91;
theorem
(1 <= r & r <= sqrt 2 & arccosec2 r = PI/4 implies r = sqrt 2) & (1 <=
r & r <= sqrt 2 & arccosec2 r = PI/2 implies r = 1) by Th32,Th92;
theorem Th105:
1 <= r & r <= sqrt 2 implies 0 <= arcsec1 r & arcsec1 r <= PI/4
proof
assume 1 <= r & r <= sqrt 2;
then
A1: r in [.1,sqrt 2.];
then r in dom (arcsec1 | [.1,sqrt 2.]) by Th45,RELAT_1:62;
then (arcsec1 | [.1,sqrt 2.]).r in rng(arcsec1 | [.1,sqrt 2.]) by
FUNCT_1:def 3;
then arcsec1 r in rng(arcsec1 | [.1,sqrt 2.]) by A1,FUNCT_1:49;
hence thesis by Th97,XXREAL_1:1;
end;
theorem Th106:
-sqrt 2 <= r & r <= -1 implies 3/4*PI <= arcsec2 r & arcsec2 r <= PI
proof
assume -sqrt 2 <= r & r <= -1;
then
A1: r in [.-sqrt 2,-1.];
then r in dom (arcsec2 | [.-sqrt 2,-1.]) by Th46,RELAT_1:62;
then (arcsec2 | [.-sqrt 2,-1.]).r in rng(arcsec2 | [.-sqrt 2,-1.]) by
FUNCT_1:def 3;
then arcsec2 r in rng(arcsec2 | [.-sqrt 2,-1.]) by A1,FUNCT_1:49;
hence thesis by Th98,XXREAL_1:1;
end;
theorem Th107:
-sqrt 2 <= r & r <= -1 implies -PI/2 <= arccosec1 r & arccosec1 r <= -PI/4
proof
assume -sqrt 2 <= r & r <= -1;
then
A1: r in [.-sqrt 2,-1.];
then r in dom (arccosec1 | [.-sqrt 2,-1.]) by Th47,RELAT_1:62;
then (arccosec1 | [.-sqrt 2,-1.]).r in rng(arccosec1 | [.-sqrt 2,-1.]) by
FUNCT_1:def 3;
then arccosec1 r in rng(arccosec1 | [.-sqrt 2,-1.]) by A1,FUNCT_1:49;
hence thesis by Th99,XXREAL_1:1;
end;
theorem Th108:
1 <= r & r <= sqrt 2 implies PI/4 <= arccosec2 r & arccosec2 r <= PI/2
proof
assume 1 <= r & r <= sqrt 2;
then
A1: r in [.1,sqrt 2.];
then r in dom (arccosec2 | [.1,sqrt 2.]) by Th48,RELAT_1:62;
then (arccosec2 | [.1,sqrt 2.]).r in rng(arccosec2 | [.1,sqrt 2.]) by
FUNCT_1:def 3;
then arccosec2 r in rng(arccosec2 | [.1,sqrt 2.]) by A1,FUNCT_1:49;
hence thesis by Th100,XXREAL_1:1;
end;
theorem Th109:
1 < r & r < sqrt 2 implies 0 < arcsec1 r & arcsec1 r < PI/4
proof
assume
A1: 1 < r & r < sqrt 2;
then arcsec1 r <= PI/4 by Th105;
then
0 < arcsec1 r & arcsec1 r < PI/4 or 0 = arcsec1 r or arcsec1 r = PI/4 by A1
,Th105,XXREAL_0:1;
hence thesis by A1,Th31,Th89;
end;
theorem Th110:
-sqrt 2 < r & r < -1 implies 3/4*PI < arcsec2 r & arcsec2 r < PI
proof
assume
A1: -sqrt 2 < r & r < -1;
then 3/4*PI <= arcsec2 r & arcsec2 r <= PI by Th106;
then
3/4*PI < arcsec2 r & arcsec2 r < PI or 3/4*PI = arcsec2 r or arcsec2 r =
PI by XXREAL_0:1;
hence thesis by A1,Th31,Th90;
end;
theorem Th111:
-sqrt 2 < r & r < -1 implies -PI/2 < arccosec1 r & arccosec1 r < -PI/4
proof
assume
A1: -sqrt 2 < r & r < -1;
then -PI/2 <= arccosec1 r & arccosec1 r <= -PI/4 by Th107;
then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 or -PI/2 = arccosec1 r or
arccosec1 r = -PI/4 by XXREAL_0:1;
hence thesis by A1,Th32,Th91;
end;
theorem Th112:
1 < r & r < sqrt 2 implies PI/4 < arccosec2 r & arccosec2 r < PI/2
proof
assume
A1: 1 < r & r < sqrt 2;
then PI/4 <= arccosec2 r & arccosec2 r <= PI/2 by Th108;
then PI/4 < arccosec2 r & arccosec2 r < PI/2 or PI/4 = arccosec2 r or
arccosec2 r = PI/2 by XXREAL_0:1;
hence thesis by A1,Th32,Th92;
end;
theorem Th113:
1 <= r & r <= sqrt 2 implies sin.(arcsec1 r) = sqrt(r^2-1)/r &
cos.(arcsec1 r) = 1/r
proof
set x = arcsec1 r;
assume that
A1: 1 <= r and
A2: r <= sqrt 2;
r in [.1,sqrt 2.] by A1,A2;
then
A3: x in dom (sec | [.0,PI/4.]) by Lm29,Th85;
PI/4 < PI/1 by XREAL_1:76;
then 0 in [.0,PI.] & PI/4 in [.0,PI.];
then [.0,PI/4.] c= [.0,PI.] by XXREAL_2:def 12;
then
A4: sin.x >= 0 by A3,Lm29,COMPTRIG:8;
A5: dom (sec | [.0,PI/4.]) c= dom sec by RELAT_1:60;
A6: r = (cos^).x by A1,A2,Th89
.= 1/cos.x by A3,A5,RFUNCT_1:def 2;
r^2 >= 1^2 by A1,SQUARE_1:15;
then
A7: r^2-1 >= 0 by XREAL_1:48;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
then (sin.x)^2 = 1-(cos.x)^2 .= 1-(1/r)*(1/r) by A6
.= 1-1/(r^2) by XCMPLX_1:102
.= (r^2)/(r^2)-1/(r^2) by A1,XCMPLX_1:60
.= (r^2-1)/(r^2);
then sin.x = sqrt ((r^2-1)/(r^2)) by A4,SQUARE_1:def 2
.= sqrt(r^2-1)/sqrt(r^2) by A1,A7,SQUARE_1:30
.= sqrt(r^2-1)/r by A1,SQUARE_1:22;
hence thesis by A6;
end;
theorem Th114:
-sqrt 2 <= r & r <= -1 implies sin.(arcsec2 r) = -sqrt(r^2-1)/r
& cos.(arcsec2 r) = 1/r
proof
3/4*PI <= PI by Lm6,XXREAL_1:2;
then
A1: 3/4*PI in [.0,PI.];
A2: dom (sec | [.3/4*PI,PI.]) c= dom sec by RELAT_1:60;
set x = arcsec2 r;
assume that
A3: -sqrt 2 <= r and
A4: r <= -1;
r in [.-sqrt 2,-1.] by A3,A4;
then
A5: x in dom (sec | [.3/4*PI,PI.]) by Lm30,Th86;
A6: r = (cos^).x by A3,A4,Th90
.= 1/cos.x by A5,A2,RFUNCT_1:def 2;
PI in [.0,PI.];
then [.3/4*PI,PI.] c= [.0,PI.] by A1,XXREAL_2:def 12;
then
A7: sin.x >= 0 by A5,Lm30,COMPTRIG:8;
-r >= -(-1) by A4,XREAL_1:24;
then (-r)^2 >= 1^2 by SQUARE_1:15;
then
A8: r^2-1 >= 0 by XREAL_1:48;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
then (sin.x)^2 = 1-(cos.x)^2 .= 1-(1/r)*(1/r) by A6
.= 1-1/(r^2) by XCMPLX_1:102
.= (r^2)/(r^2)-1/(r^2) by A4,XCMPLX_1:60
.= (r^2-1)/(r^2);
then sin.x = sqrt ((r^2-1)/(r^2)) by A7,SQUARE_1:def 2
.= sqrt(r^2-1)/sqrt(r^2) by A4,A8,SQUARE_1:30
.= sqrt(r^2-1)/(-r) by A4,SQUARE_1:23
.= -sqrt(r^2-1)/r by XCMPLX_1:188;
hence thesis by A6;
end;
theorem Th115:
-sqrt 2 <= r & r <= -1 implies sin.(arccosec1 r) = 1/r & cos.(
arccosec1 r) = -sqrt(r^2-1)/r
proof
set x = arccosec1 r;
assume that
A1: -sqrt 2 <= r and
A2: r <= -1;
r in [.-sqrt 2,-1.] by A1,A2;
then
A3: x in dom (cosec | [.-PI/2,-PI/4.]) by Lm31,Th87;
-PI/4 >= -PI/2 by Lm7,XXREAL_1:3;
then -PI/2 in [.-PI/2,PI/2.] & -PI/4 in [.-PI/2,PI/2.];
then [.-PI/2,-PI/4.] c= [.-PI/2,PI/2.] by XXREAL_2:def 12;
then
A4: cos.x >= 0 by A3,Lm31,COMPTRIG:12;
A5: dom (cosec | [.-PI/2,-PI/4.]) c= dom cosec by RELAT_1:60;
A6: r = (sin^).x by A1,A2,Th91
.= 1/sin.x by A3,A5,RFUNCT_1:def 2;
-r >= -(-1) by A2,XREAL_1:24;
then (-r)^2 >= 1^2 by SQUARE_1:15;
then
A7: r^2-1 >= 0 by XREAL_1:48;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
then (cos.x)^2 = 1-(sin.x)^2 .= 1-(1/r)*(1/r) by A6
.= 1-1/(r^2) by XCMPLX_1:102
.= (r^2)/(r^2)-1/(r^2) by A2,XCMPLX_1:60
.= (r^2-1)/(r^2);
then cos.x = sqrt ((r^2-1)/(r^2)) by A4,SQUARE_1:def 2
.= sqrt(r^2-1)/sqrt(r^2) by A2,A7,SQUARE_1:30
.= sqrt(r^2-1)/(-r) by A2,SQUARE_1:23
.= -sqrt(r^2-1)/r by XCMPLX_1:188;
hence thesis by A6;
end;
theorem Th116:
1 <= r & r <= sqrt 2 implies sin.(arccosec2 r) = 1/r & cos.(
arccosec2 r) = sqrt(r^2-1)/r
proof
PI/4 <= PI/2 by Lm8,XXREAL_1:2;
then
A1: PI/4 in [.-PI/2,PI/2.];
A2: dom (cosec | [.PI/4,PI/2.]) c= dom cosec by RELAT_1:60;
set x = arccosec2 r;
assume that
A3: 1 <= r and
A4: r <= sqrt 2;
r in [.1,sqrt 2.] by A3,A4;
then
A5: x in dom (cosec | [.PI/4,PI/2.]) by Lm32,Th88;
A6: r = (sin^).x by A3,A4,Th92
.= 1/sin.x by A5,A2,RFUNCT_1:def 2;
PI/2 in [.-PI/2,PI/2.];
then [.PI/4,PI/2.] c= [.-PI/2,PI/2.] by A1,XXREAL_2:def 12;
then
A7: cos.x >= 0 by A5,Lm32,COMPTRIG:12;
r^2 >= 1^2 by A3,SQUARE_1:15;
then
A8: r^2-1 >= 0 by XREAL_1:48;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:28;
then (cos.x)^2 = 1-(sin.x)^2 .= 1-(1/r)*(1/r) by A6
.= 1-1/(r^2) by XCMPLX_1:102
.= (r^2)/(r^2)-1/(r^2) by A3,XCMPLX_1:60
.= (r^2-1)/(r^2);
then cos.x = sqrt ((r^2-1)/(r^2)) by A7,SQUARE_1:def 2
.= sqrt(r^2-1)/sqrt(r^2) by A3,A8,SQUARE_1:30
.= sqrt(r^2-1)/r by A3,SQUARE_1:22;
hence thesis by A6;
end;
theorem
1 < r & r < sqrt 2 implies cosec.(arcsec1 r) = r/sqrt(r^2-1)
proof
set x = arcsec1 r;
].0,PI/2.] = ].0,PI/2.[ \/ {PI/2} by XXREAL_1:132;
then
A1: ].0,PI/2.[ c= ].0,PI/2.] by XBOOLE_1:7;
PI/4 < PI/2 by XREAL_1:76;
then ].0,PI/4.[ c= ].0,PI/2.[ by XXREAL_1:46;
then ].0,PI/4.[ c= ].0,PI/2.] by A1;
then
A2: ].0,PI/4.[ c= dom cosec by Th4;
assume
A3: 1 < r & r < sqrt 2;
then 0 < arcsec1 r & arcsec1 r < PI/4 by Th109;
then x in ].0,PI/4.[;
then cosec.x = 1/sin.x by A2,RFUNCT_1:def 2
.= 1/(sqrt(r^2-1)/r) by A3,Th113
.= r/sqrt(r^2-1) by XCMPLX_1:57;
hence thesis;
end;
theorem
-sqrt 2 < r & r < -1 implies cosec.(arcsec2 r) = -r/sqrt(r^2-1)
proof
set x = arcsec2 r;
A1: ].3/4*PI,PI.[ c= dom cosec
proof
].3/4*PI,PI.[ /\ sin"{0} = {}
proof
assume ].3/4*PI,PI.[ /\ sin"{0} <> {};
then consider rr being object such that
A2: rr in ].3/4*PI,PI.[ /\ sin"{0} by XBOOLE_0:def 1;
rr in sin"{0} by A2,XBOOLE_0:def 4;
then
A3: sin.rr in {0} by FUNCT_1:def 7;
A4: ].3/4*PI,PI.[ c= ].0,PI.[ by XXREAL_1:46;
rr in ].3/4*PI,PI.[ by A2,XBOOLE_0:def 4;
then sin.rr <> 0 by A4,COMPTRIG:7;
hence contradiction by A3,TARSKI:def 1;
end;
then ].3/4*PI,PI.[ \ sin"{0} c= dom sin \ sin"{0} & ].3/4*PI,PI.[ misses
sin"{0} by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then ].3/4*PI,PI.[ c= dom sin \ sin"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
assume
A5: -sqrt 2 < r & r < -1;
then 3/4*PI < arcsec2 r & arcsec2 r < PI by Th110;
then x in ].3/4*PI,PI.[;
then cosec.x = 1/sin.x by A1,RFUNCT_1:def 2
.= 1/(-sqrt(r^2-1)/r) by A5,Th114
.= -1/(sqrt(r^2-1)/r) by XCMPLX_1:188
.= -r/sqrt(r^2-1) by XCMPLX_1:57;
hence thesis;
end;
theorem
-sqrt 2 < r & r < -1 implies sec.(arccosec1 r) = -r/sqrt(r^2-1)
proof
set x = arccosec1 r;
A1: ].-PI/2,-PI/4.[ c= dom sec
proof
].-PI/2,-PI/4.[ /\ cos"{0} = {}
proof
assume ].-PI/2,-PI/4.[ /\ cos"{0} <> {};
then consider rr being object such that
A2: rr in ].-PI/2,-PI/4.[ /\ cos"{0} by XBOOLE_0:def 1;
rr in cos"{0} by A2,XBOOLE_0:def 4;
then
A3: cos.rr in {0} by FUNCT_1:def 7;
A4: ].-PI/2,-PI/4.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
rr in ].-PI/2,-PI/4.[ by A2,XBOOLE_0:def 4;
then cos.rr <> 0 by A4,COMPTRIG:11;
hence contradiction by A3,TARSKI:def 1;
end;
then ].-PI/2,-PI/4.[ \ cos"{0} c= dom cos \ cos"{0} & ].-PI/2,-PI/4.[
misses cos" {0} by SIN_COS:24,XBOOLE_0:def 7,XBOOLE_1:33;
then ].-PI/2,-PI/4.[ c= dom cos \ cos"{0} by XBOOLE_1:83;
hence thesis by RFUNCT_1:def 2;
end;
assume
A5: -sqrt 2 < r & r < -1;
then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 by Th111;
then x in ].-PI/2,-PI/4.[;
then sec.x = 1/cos.x by A1,RFUNCT_1:def 2
.= 1/(-sqrt(r^2-1)/r) by A5,Th115
.= -1/(sqrt(r^2-1)/r) by XCMPLX_1:188
.= -r/sqrt(r^2-1) by XCMPLX_1:57;
hence thesis;
end;
theorem
1 < r & r < sqrt 2 implies sec.(arccosec2 r) = r/sqrt(r^2-1)
proof
set x = arccosec2 r;
[.0,PI/2.[ = ].0,PI/2.[ \/ {0} by XXREAL_1:131;
then ].PI/4,PI/2.[ c= ].0,PI/2.[ & ].0,PI/2.[ c= [.0,PI/2.[ by XBOOLE_1:7
,XXREAL_1:46;
then ].PI/4,PI/2.[ c= [.0,PI/2.[;
then
A1: ].PI/4,PI/2.[ c= dom sec by Th1;
assume
A2: 1 < r & r < sqrt 2;
then PI/4 < arccosec2 r & arccosec2 r < PI/2 by Th112;
then x in ].PI/4,PI/2.[;
then sec.x = 1/cos.x by A1,RFUNCT_1:def 2
.= 1/(sqrt(r^2-1)/r) by A2,Th116
.= r/sqrt(r^2-1) by XCMPLX_1:57;
hence thesis;
end;
theorem Th121:
arcsec1 is_differentiable_on sec.:].0,PI/2.[
proof
set X = sec.:].0,PI/2.[;
set g1 = arcsec1|(sec.:].0,PI/2.[);
set f = sec|[.0,PI/2.[;
set g = f|].0,PI/2.[;
A1: g = sec|].0,PI/2.[ by RELAT_1:74,XXREAL_1:22;
A2: dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:33
.= rng(sec|].0,PI/2.[) by A1,RELAT_1:72
.= sec.:].0,PI/2.[ by RELAT_1:115;
A3: (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:72
.= arcsec1|(f.:].0,PI/2.[) by RFUNCT_2:17
.= arcsec1|(rng(f|].0,PI/2.[)) by RELAT_1:115
.= arcsec1|(rng (sec|].0,PI/2.[)) by RELAT_1:74,XXREAL_1:22
.= arcsec1|(sec.:].0,PI/2.[) by RELAT_1:115;
A4: g is_differentiable_on ].0,PI/2.[ by A1,Th5,FDIFF_2:16;
now
A5: for x0 st x0 in ].0,PI/2.[ holds sin.x0/(cos.x0)^2 > 0
proof
let x0;
assume
A6: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A7: cos.x0 > 0 by A6,COMPTRIG:11;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
then sin.x0 > 0 by A6,COMPTRIG:7;
hence thesis by A7;
end;
let x0 such that
A8: x0 in ].0,PI/2.[;
diff(g,x0) = (g`|].0,PI/2.[).x0 by A4,A8,FDIFF_1:def 7
.= ((sec|].0,PI/2.[)`|].0,PI/2.[).x0 by RELAT_1:74,XXREAL_1:22
.= (sec`|].0,PI/2.[).x0 by Th5,FDIFF_2:16
.= diff(sec,x0) by A8,Th5,FDIFF_1:def 7
.= sin.x0/(cos.x0)^2 by A8,Th5;
hence diff(g,x0) > 0 by A8,A5;
end;
then
A9: g1 is_differentiable_on X by A2,A4,A3,Lm21,FDIFF_2:48;
A10: for x st x in X holds arcsec1|X is_differentiable_in x
proof
let x;
assume x in X;
then g1|X is_differentiable_in x by A9,FDIFF_1:def 6;
hence thesis by RELAT_1:72;
end;
X c= dom arcsec1 by A2,A3,RELAT_1:60;
hence thesis by A10,FDIFF_1:def 6;
end;
theorem Th122:
arcsec2 is_differentiable_on sec.:].PI/2,PI.[
proof
set X = sec.:].PI/2,PI.[;
set g1 = arcsec2|(sec.:].PI/2,PI.[);
set f = sec|].PI/2,PI.];
set g = f|].PI/2,PI.[;
A1: g = sec|].PI/2,PI.[ by RELAT_1:74,XXREAL_1:21;
A2: dom ((g|].PI/2,PI.[)") = rng (g|].PI/2,PI.[) by FUNCT_1:33
.= rng(sec|].PI/2,PI.[) by A1,RELAT_1:72
.= sec.:].PI/2,PI.[ by RELAT_1:115;
A3: (g|].PI/2,PI.[)" = (f|].PI/2,PI.[)" by RELAT_1:72
.= arcsec2|(f.:].PI/2,PI.[) by RFUNCT_2:17
.= arcsec2|(rng(f|].PI/2,PI.[)) by RELAT_1:115
.= arcsec2|(rng (sec|].PI/2,PI.[)) by RELAT_1:74,XXREAL_1:21
.= arcsec2|(sec.:].PI/2,PI.[) by RELAT_1:115;
A4: g is_differentiable_on ].PI/2,PI.[ by A1,Th6,FDIFF_2:16;
now
A5: for x0 st x0 in ].PI/2,PI.[ holds sin.x0/(cos.x0)^2 > 0
proof
let x0;
assume
A6: x0 in ].PI/2,PI.[;
].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:5,XXREAL_1:46;
then
A7: cos.x0 < 0 by A6,COMPTRIG:13;
].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;
then sin.x0 > 0 by A6,COMPTRIG:7;
hence thesis by A7;
end;
let x0 such that
A8: x0 in ].PI/2,PI.[;
diff(g,x0) = (g`|].PI/2,PI.[).x0 by A4,A8,FDIFF_1:def 7
.= ((sec|].PI/2,PI.[)`|].PI/2,PI.[).x0 by RELAT_1:74,XXREAL_1:21
.= (sec`|].PI/2,PI.[).x0 by Th6,FDIFF_2:16
.= diff(sec,x0) by A8,Th6,FDIFF_1:def 7
.= sin.x0/(cos.x0)^2 by A8,Th6;
hence diff(g,x0) > 0 by A8,A5;
end;
then
A9: g1 is_differentiable_on X by A2,A4,A3,Lm22,FDIFF_2:48;
A10: for x st x in X holds arcsec2|X is_differentiable_in x
proof
let x;
assume x in X;
then g1|X is_differentiable_in x by A9,FDIFF_1:def 6;
hence thesis by RELAT_1:72;
end;
X c= dom arcsec2 by A2,A3,RELAT_1:60;
hence thesis by A10,FDIFF_1:def 6;
end;
theorem Th123:
arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
proof
set X = cosec.:].-PI/2,0.[;
set g1 = arccosec1|(cosec.:].-PI/2,0.[);
set f = cosec|[.-PI/2,0.[;
set g = f|].-PI/2,0.[;
A1: g = cosec|].-PI/2,0.[ by RELAT_1:74,XXREAL_1:22;
A2: dom ((g|].-PI/2,0.[)") = rng (g|].-PI/2,0.[) by FUNCT_1:33
.= rng(cosec|].-PI/2,0.[) by A1,RELAT_1:72
.= cosec.:].-PI/2,0.[ by RELAT_1:115;
A3: (g|].-PI/2,0.[)" = (f|].-PI/2,0.[)" by RELAT_1:72
.= arccosec1|(f.:].-PI/2,0.[) by RFUNCT_2:17
.= arccosec1|(rng(f|].-PI/2,0.[)) by RELAT_1:115
.= arccosec1|(rng (cosec|].-PI/2,0.[)) by RELAT_1:74,XXREAL_1:22
.= arccosec1|(cosec.:].-PI/2,0.[) by RELAT_1:115;
A4: g is_differentiable_on ].-PI/2,0.[ by A1,Th7,FDIFF_2:16;
now
A5: for x0 st x0 in ].-PI/2,0.[ holds -cos.x0/(sin.x0)^2 < 0
proof
let x0;
assume
A6: x0 in ].-PI/2,0.[;
then x0 < 0 by XXREAL_1:4;
then
A7: x0+2*PI < 0+2*PI by XREAL_1:8;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by XXREAL_1:131;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3;
then -PI < x0 by A6,XXREAL_1:4;
then -PI+2*PI < x0+2*PI by XREAL_1:8;
then x0+2*PI in ].PI,2*PI.[ by A7;
then sin.(x0+2*PI) < 0 by COMPTRIG:9;
then
A8: sin.x0 < 0 by SIN_COS:78;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then cos.x0 > 0 by A6,COMPTRIG:11;
hence thesis by A8;
end;
let x0 such that
A9: x0 in ].-PI/2,0.[;
diff(g,x0) = (g`|].-PI/2,0.[).x0 by A4,A9,FDIFF_1:def 7
.= ((cosec|].-PI/2,0.[)`|].-PI/2,0.[).x0 by RELAT_1:74,XXREAL_1:22
.= (cosec`|].-PI/2,0.[).x0 by Th7,FDIFF_2:16
.= diff(cosec,x0) by A9,Th7,FDIFF_1:def 7
.= -cos.x0/(sin.x0)^2 by A9,Th7;
hence diff(g,x0) < 0 by A9,A5;
end;
then
A10: g1 is_differentiable_on X by A2,A4,A3,Lm23,FDIFF_2:48;
A11: for x st x in X holds arccosec1|X is_differentiable_in x
proof
let x;
assume x in X;
then g1|X is_differentiable_in x by A10,FDIFF_1:def 6;
hence thesis by RELAT_1:72;
end;
X c= dom arccosec1 by A2,A3,RELAT_1:60;
hence thesis by A11,FDIFF_1:def 6;
end;
theorem Th124:
arccosec2 is_differentiable_on cosec.:].0,PI/2.[
proof
set X = cosec.:].0,PI/2.[;
set g1 = arccosec2|(cosec.:].0,PI/2.[);
set f = cosec|].0,PI/2.];
set g = f|].0,PI/2.[;
A1: g = cosec|].0,PI/2.[ by RELAT_1:74,XXREAL_1:21;
A2: dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:33
.= rng(cosec|].0,PI/2.[) by A1,RELAT_1:72
.= cosec.:].0,PI/2.[ by RELAT_1:115;
A3: (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:72
.= arccosec2|(f.:].0,PI/2.[) by RFUNCT_2:17
.= arccosec2|(rng(f|].0,PI/2.[)) by RELAT_1:115
.= arccosec2|(rng (cosec|].0,PI/2.[)) by RELAT_1:74,XXREAL_1:21
.= arccosec2|(cosec.:].0,PI/2.[) by RELAT_1:115;
A4: g is_differentiable_on ].0,PI/2.[ by A1,Th8,FDIFF_2:16;
now
A5: for x0 st x0 in ].0,PI/2.[ holds -cos.x0/(sin.x0)^2 < 0
proof
let x0;
assume
A6: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A7: cos.x0 > 0 by A6,COMPTRIG:11;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
then sin.x0 > 0 by A6,COMPTRIG:7;
hence thesis by A7;
end;
let x0 such that
A8: x0 in ].0,PI/2.[;
diff(g,x0) = (g`|].0,PI/2.[).x0 by A4,A8,FDIFF_1:def 7
.= ((cosec|].0,PI/2.[)`|].0,PI/2.[).x0 by RELAT_1:74,XXREAL_1:21
.= (cosec`|].0,PI/2.[).x0 by Th8,FDIFF_2:16
.= diff(cosec,x0) by A8,Th8,FDIFF_1:def 7
.= -cos.x0/(sin.x0)^2 by A8,Th8;
hence diff(g,x0) < 0 by A8,A5;
end;
then
A9: g1 is_differentiable_on X by A2,A4,A3,Lm24,FDIFF_2:48;
A10: for x st x in X holds arccosec2|X is_differentiable_in x
proof
let x;
assume x in X;
then g1|X is_differentiable_in x by A9,FDIFF_1:def 6;
hence thesis by RELAT_1:72;
end;
X c= dom arccosec2 by A2,A3,RELAT_1:60;
hence thesis by A10,FDIFF_1:def 6;
end;
theorem
sec.:].0,PI/2.[ is open
proof
for x0 st x0 in ].0,PI/2.[ holds diff(sec,x0) > 0
proof
let x0;
assume
A1: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A2: cos.x0 > 0 by A1,COMPTRIG:11;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
then sin.x0 > 0 by A1,COMPTRIG:7;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2;
hence thesis by A1,Th5;
end;
then rng(sec|].0,PI/2.[) is open by Lm10,Th5,FDIFF_2:41;
hence thesis by RELAT_1:115;
end;
theorem
sec.:].PI/2,PI.[ is open
proof
for x0 st x0 in ].PI/2,PI.[ holds diff(sec,x0) > 0
proof
let x0;
assume
A1: x0 in ].PI/2,PI.[;
].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:5,XXREAL_1:46;
then
A2: cos.x0 < 0 by A1,COMPTRIG:13;
].PI/2,PI.[ c= ].0,PI.[ by XXREAL_1:46;
then sin.x0 > 0 by A1,COMPTRIG:7;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2;
hence thesis by A1,Th6;
end;
then rng(sec|].PI/2,PI.[) is open by Lm12,Th6,FDIFF_2:41;
hence thesis by RELAT_1:115;
end;
theorem
cosec.:].-PI/2,0.[ is open
proof
for x0 st x0 in ].-PI/2,0.[ holds diff(cosec,x0) < 0
proof
let x0;
assume
A1: x0 in ].-PI/2,0.[;
then x0 < 0 by XXREAL_1:4;
then
A2: x0+2*PI < 0+2*PI by XREAL_1:8;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by XXREAL_1:131;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3;
then -PI < x0 by A1,XXREAL_1:4;
then -PI+2*PI < x0+2*PI by XREAL_1:8;
then x0+2*PI in ].PI,2*PI.[ by A2;
then sin.(x0+2*PI) < 0 by COMPTRIG:9;
then
A3: sin.x0 < 0 by SIN_COS:78;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then cos.x0 > 0 by A1,COMPTRIG:11;
then -(cos.x0/(sin.x0)^2) < -0 by A3;
hence thesis by A1,Th7;
end;
then rng(cosec|].-PI/2,0.[) is open by Lm16,Th7,FDIFF_2:41;
hence thesis by RELAT_1:115;
end;
theorem
cosec.:].0,PI/2.[ is open
proof
for x0 st x0 in ].0,PI/2.[ holds diff(cosec,x0) < 0
proof
let x0;
assume
A1: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by XXREAL_1:46;
then
A2: cos.x0 > 0 by A1,COMPTRIG:11;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:5,XXREAL_1:46;
then sin.x0 > 0 by A1,COMPTRIG:7;
then -(cos.x0/(sin.x0)^2) < -0 by A2;
hence thesis by A1,Th8;
end;
then rng(cosec|].0,PI/2.[) is open by Lm18,Th8,FDIFF_2:41;
hence thesis by RELAT_1:115;
end;
theorem
arcsec1|(sec.:].0,PI/2.[) is continuous by Th121,FDIFF_1:25;
theorem
arcsec2|(sec.:].PI/2,PI.[) is continuous by Th122,FDIFF_1:25;
theorem
arccosec1|(cosec.:].-PI/2,0.[) is continuous by Th123,FDIFF_1:25;
theorem
arccosec2|(cosec.:].0,PI/2.[) is continuous by Th124,FDIFF_1:25;