:: Inverse Trigonometric Functions Arcsec and Arccosec
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies FUNCT_1, RELAT_1, PRE_TOPC, ARYTM_1, ARYTM_3, PARTFUN1, SIN_COS,
FDIFF_1, SQUARE_1, FINSEQ_1, SIN_COS4, ORDINAL2, ARYTM, BOOLE, SEQ_1,
RCOMP_1, INT_1, FCONT_1, RFUNCT_2, SINCOS10, SEQ_2;
notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, FUNCT_1, RELSET_1, PARTFUN1,
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,
RCOMP_2, SEQ_2;
constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
SIN_COS, PARTFUN2, SIN_COS4, TOPALG_2, FDIFF_9, RCOMP_2, SEQ_1, SEQ_2;
registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
FUNCT_1, SIN_COS6, RFUNCT_2, ORDINAL1, INT_1, VALUED_0;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI, FDIFF_9, XCMPLX_0, RCOMP_2, RFUNCT_2, SQUARE_1;
theorems SIN_COS6, FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG,
RFUNCT_2, FCONT_1, FUNCT_1, RCOMP_1, REAL_1, XBOOLE_0, SQUARE_1, FCONT_3,
XREAL_1, TARSKI, XBOOLE_1, ROLLE, RFUNCT_1, REAL_2, FCONT_2, SEQ_1,
FDIFF_9, RCOMP_2, XXREAL_0, FUNCT_2;
begin :: arcsec, arccosec
reserve x, r, s, h for Real,
a, b, p, q, th for real number,
i for integer number,
n for Element of NAT,
rr, y for set,
Z for open Subset of REAL,
X, Y for Subset of REAL,
rseq for Real_Sequence,
f, f1, f2, g for PartFunc of REAL,REAL;
Lm1:
[.0,PI/2.[ c= ].-PI/2,PI/2.[
proof
PI in ].0,4.[ by SIN_COS:def 32;then
PI > 0 by RCOMP_1:47;then
A2: 0/2 < PI/2 by XREAL_1:76;
A3: 0 - PI/2 < 0 by XREAL_1:51;
A4: ].0,PI/2.[ c= ].-PI/2,PI/2.[ by A3,RCOMP_1:52;
0 - PI < 0 by XREAL_1:51;
then (-PI)/2 < 0/2 by XREAL_1:76;then
A5: 0 in ].-PI/2,PI/2.[ by A2,RCOMP_1:47;
{0} c= ].-PI/2,PI/2.[
proof
let x be set;
assume x in {0};
hence x in ].-PI/2,PI/2.[ by A5,TARSKI:def 1;
end;
then ].0,PI/2.[ \/ {0} c= ].-PI/2,PI/2.[ by A4,XBOOLE_1:8;
hence [.0,PI/2.[ c= ].-PI/2,PI/2.[ by A2,RCOMP_2:5;
end;
theorem Th1:
[.0,PI/2.[ c= dom sec
proof
set f = cos^;
A1: [.0,PI/2.[ \ cos"{0} c= dom cos \ cos"{0} by SIN_COS:27,XBOOLE_1:33;
[.0,PI/2.[ /\ cos"{0} = {}
proof
assume [.0,PI/2.[ /\ cos"{0} <> {};
then consider rr such that
A2: rr in [.0,PI/2.[ /\ cos"{0} by XBOOLE_0:def 1;
A3: rr in [.0,PI/2.[ & rr in cos"{0} by A2,XBOOLE_0:def 3;then
A4: rr is Real;
A5: cos.rr <> 0 by A3,A4,Lm1,COMPTRIG:27;
cos.(rr) in {0} by A3,FUNCT_1:def 13;
hence contradiction by A5,TARSKI:def 1;
end;
then [.0,PI/2.[ misses cos"{0} by XBOOLE_0:def 7;
then [.0,PI/2.[ c= dom cos \ cos"{0} by A1,XBOOLE_1:83;
hence [.0,PI/2.[ c= dom sec by RFUNCT_1:def 8;
end;
Lm2:
].PI/2,PI.] c= ].PI/2,3/2*PI.[
proof
PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by RCOMP_1:47;then
A2: PI < 3/2*PI by REAL_2:144;
A3: ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by A2,RCOMP_1:52;
A4: PI/2 < PI/1 by A1,REAL_2:200;then
A5: PI in ].PI/2,3/2*PI.[ by A2,RCOMP_1:47;
{PI} c= ].PI/2,3/2*PI.[
proof
let x be set;
assume x in {PI};
hence x in ].PI/2,3/2*PI.[ by A5,TARSKI:def 1;
end;
then ].PI/2,PI.[ \/ {PI} c= ].PI/2,3/2*PI.[ by A3,XBOOLE_1:8;
hence ].PI/2,PI.] c= ].PI/2,3/2*PI.[ by A4,RCOMP_2:6;
end;
theorem Th2:
].PI/2,PI.] c= dom sec
proof
set f = cos^;
A1: ].PI/2,PI.] \ cos"{0} c= dom cos \ cos"{0} by SIN_COS:27,XBOOLE_1:33;
].PI/2,PI.] /\ cos"{0} = {}
proof
assume ].PI/2,PI.] /\ cos"{0} <> {};
then consider rr such that
A2: rr in ].PI/2,PI.] /\ cos"{0} by XBOOLE_0:def 1;
A3: rr in ].PI/2,PI.] & rr in cos"{0} by A2,XBOOLE_0:def 3;then
A4: rr is Real;
A5: cos.rr <> 0 by A3,A4,Lm2,COMPTRIG:29;
cos.(rr) in {0} by A3,FUNCT_1:def 13;
hence contradiction by A5,TARSKI:def 1;
end;
then ].PI/2,PI.] misses cos"{0} by XBOOLE_0:def 7;
then ].PI/2,PI.] c= dom cos \ cos"{0} by A1,XBOOLE_1:83;
hence ].PI/2,PI.] c= dom sec by RFUNCT_1:def 8;
end;
Lm3:
[.-PI/2,0.[ c= ].-PI,0.[
proof
PI in ].0,4.[ by SIN_COS:def 32;then
PI > 0 by RCOMP_1:47;
then PI/2 < PI/1 by REAL_2:200;then
A2: -PI < -PI/2 by XREAL_1:26;then
A3: ].-PI/2,0.[ c= ].-PI,0.[ by RCOMP_1:52;
A4: -PI/2 < -0 by XREAL_1:26;then
A5: -PI/2 in ].-PI,0.[ by A2,RCOMP_1:47;
{-PI/2} c= ].-PI,0.[
proof
let x be set;
assume x in {-PI/2};
hence x in ].-PI,0.[ by A5,TARSKI:def 1;
end;
then ].-PI/2,0.[ \/ {-PI/2} c= ].-PI,0.[ by A3,XBOOLE_1:8;
hence [.-PI/2,0.[ c= ].-PI,0.[ by A4,RCOMP_2:5;
end;
theorem Th3:
[.-PI/2,0.[ c= dom cosec
proof
set f = sin^;
A1: [.-PI/2,0.[ \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
[.-PI/2,0.[ /\ sin"{0} = {}
proof
assume [.-PI/2,0.[ /\ sin"{0} <> {};
then consider rr such that
A2: rr in [.-PI/2,0.[ /\ sin"{0} by XBOOLE_0:def 1;
A3: rr in [.-PI/2,0.[ & rr in sin"{0} by A2,XBOOLE_0:def 3;then
rr is Real;
then reconsider rr as real number;
-PI < rr & rr < 0 by A3,Lm3,RCOMP_1:47;
then -PI+2*PI < rr+2*PI & rr+2*PI < 0+2*PI by XREAL_1:10;
then rr+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(rr+2*PI) < 0 by COMPTRIG:25;then
A5: sin.rr <> 0 by SIN_COS:83;
sin.rr in {0} by A3,FUNCT_1:def 13;
hence contradiction by A5,TARSKI:def 1;
end;
then [.-PI/2,0.[ misses sin"{0} by XBOOLE_0:def 7;
then [.-PI/2,0.[ c= dom sin \ sin"{0} by A1,XBOOLE_1:83;
hence [.-PI/2,0.[ c= dom cosec by RFUNCT_1:def 8;
end;
Lm4:
].0,PI/2.] c= ].0,PI.[
proof
PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by RCOMP_1:47;then
A2: PI/2 < PI/1 by REAL_2:200;then
A3: ].0,PI/2.[ c= ].0,PI.[ by RCOMP_1:52;
A4: PI/2 > 0/2 by A1,XREAL_1:76;then
A5: PI/2 in ].0,PI.[ by A2,RCOMP_1:47;
{PI/2} c= ].0,PI.[
proof
let x be set;
assume x in {PI/2};
hence x in ].0,PI.[ by A5,TARSKI:def 1;
end;
then ].0,PI/2.[ \/ {PI/2} c= ].0,PI.[ by A3,XBOOLE_1:8;
hence ].0,PI/2.] c= ].0,PI.[ by A4,RCOMP_2:6;
end;
theorem Th4:
].0,PI/2.] c= dom cosec
proof
set f = sin^;
A1: ].0,PI/2.] \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
].0,PI/2.] /\ sin"{0} = {}
proof
assume ].0,PI/2.] /\ sin"{0} <> {};
then consider rr such that
A2: rr in ].0,PI/2.] /\ sin"{0} by XBOOLE_0:def 1;
A3: rr in ].0,PI/2.] & rr in sin"{0} by A2,XBOOLE_0:def 3;then
A4: rr is Real;
A5: sin.rr <> 0 by A3,A4,Lm4,COMPTRIG:23;
sin.rr in {0} by A3,FUNCT_1:def 13;
hence contradiction by A5,TARSKI:def 1;
end;
then ].0,PI/2.] misses sin"{0} by XBOOLE_0:def 7;
then ].0,PI/2.] c= dom sin \ sin"{0} by A1,XBOOLE_1:83;
hence ].0,PI/2.] c= dom cosec by RFUNCT_1:def 8;
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.[;
PI in ].0,4.[ by SIN_COS:def 32;
then PI > 0 by RCOMP_1:47;
then PI/2 > 0/2 by XREAL_1:76;
then [.0,PI/2.[ = Z \/ {0} by RCOMP_2:5;
then Z c= [.0,PI/2.[ by XBOOLE_1:7;then
A1: Z c= dom sec by Th1,XBOOLE_1:1;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;
diff(sec,x) = ((sec)`|Z).x by A2,A3,FDIFF_1:def 8
.= 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 in ].0,4.[ by SIN_COS:def 32;
then PI > 0 by RCOMP_1:47;
then PI/2 < PI/1 by REAL_2:200;
then ].PI/2,PI.] = Z \/ {PI} by RCOMP_2:6;
then Z c= ].PI/2,PI.] by XBOOLE_1:7;then
A1: Z c= dom sec by Th2,XBOOLE_1:1;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;
diff(sec,x) = ((sec)`|Z).x by A2,A3,FDIFF_1:def 8
.= 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 by XREAL_1:26;
then [.-PI/2,0.[ = Z \/ {-PI/2} by RCOMP_2:5;
then Z c= [.-PI/2,0.[ by XBOOLE_1:7;then
A1: Z c= dom cosec by Th3,XBOOLE_1:1;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;
diff(cosec,x) = ((cosec)`|Z).x by A2,A3,FDIFF_1:def 8
.= -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.[;
PI in ].0,4.[ by SIN_COS:def 32;
then PI > 0 by RCOMP_1:47;
then PI/2 > 0/2 by XREAL_1:76;
then ].0,PI/2.] = Z \/ {PI/2} by RCOMP_2:6;
then Z c= ].0,PI/2.] by XBOOLE_1:7;then
A1: Z c= dom cosec by Th4,XBOOLE_1:1;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;
diff(cosec,x) = ((cosec)`|Z).x by A2,A3,FDIFF_1:def 8
.= -cos.x/(sin.x)^2 by A1,A3,FDIFF_9:5;
hence thesis;
end;
hence thesis by A1,FDIFF_9:5;
end;
theorem
sec is_continuous_on ].0,PI/2.[ by Th5,FDIFF_1:33;
theorem
sec is_continuous_on ].PI/2,PI.[ by Th6,FDIFF_1:33;
theorem
cosec is_continuous_on ].-PI/2,0.[ by Th7,FDIFF_1:33;
theorem
cosec is_continuous_on ].0,PI/2.[ by Th8,FDIFF_1:33;
theorem Th13:
sec is_increasing_on ].0,PI/2.[
proof
PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by RCOMP_1:47;then
A2: PI/2 > 0/2 by XREAL_1:76;
for x be Real st x in ].0,PI/2.[ holds diff(sec,x) > 0
proof
let x be Real;
assume
A4: x in ].0,PI/2.[;
PI/2 < PI/1 by A1,REAL_2:200;
then ].0,PI/2.[ c= ].0,PI.[ by RCOMP_1:52;then
A5: sin.x > 0 by A4,COMPTRIG:23;
0 - PI/2 < 0 by XREAL_1:51;
then ].0,PI/2.[ c= ].-PI/2,PI/2.[ by RCOMP_1:52;
then cos.x > 0 by A4,COMPTRIG:27;
then (cos.x)^2 > 0 by SQUARE_1:74;
then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A5,REAL_1:73;
hence thesis by A4,Th5;
end;
hence thesis by A2,Th5,ROLLE:9;
end;
theorem Th14:
sec is_increasing_on ].PI/2,PI.[
proof
A0: PI in ].0,4.[ by SIN_COS:def 32;then
A1: PI > 0 by RCOMP_1:47;
A3: for x be Real st x in ].PI/2,PI.[ holds diff(sec,x) > 0
proof
let x be Real;
assume
A4: x in ].PI/2,PI.[;
PI/2 > 0/2 by A1,XREAL_1:76;
then ].PI/2,PI.[ c= ].0,PI.[ by RCOMP_1:52;then
A5: sin.x > 0 by A4,COMPTRIG:23;
PI > 0 by A0,RCOMP_1:47;
then PI <= 3/2*PI by REAL_2:146;
then ].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by RCOMP_1:52;
then cos.x < 0 by A4,COMPTRIG:29;
then (cos.x)^2 > 0 by SQUARE_1:74;
then sin.x/(cos.x)^2 > 0/(cos.x)^2 by A5,REAL_1:73;
hence thesis by A4,Th6;
end;
PI > 0 by A0,RCOMP_1:47;
then PI/2 < PI/1 by REAL_2:200;
hence thesis by A3,Th6,ROLLE:9;
end;
theorem Th15:
cosec is_decreasing_on ].-PI/2,0.[
proof
for x be Real st x in ].-PI/2,0.[ holds diff(cosec,x) < 0
proof
let x be Real;
assume
A2: x in ].-PI/2,0.[;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,RCOMP_2:5;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3,XBOOLE_1:1;
then -PI < x & x < 0 by A2,RCOMP_1:47;
then -PI+2*PI < x+2*PI & x+2*PI < 0+2*PI by XREAL_1:10;
then x+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(x+2*PI) < 0 by COMPTRIG:25;
then sin.x < 0 by SIN_COS:83;then
A3: (sin.x)^2 > 0 by SQUARE_1:74;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x > 0 by A2,COMPTRIG:27;
then cos.x/(sin.x)^2 > 0/(sin.x)^2 by A3,REAL_1:73;
then -cos.x/(sin.x)^2 < -0 by XREAL_1:26;
hence thesis by A2,Th7;
end;
hence thesis by Th7,COMPTRIG:21,ROLLE:10;
end;
theorem Th16:
cosec is_decreasing_on ].0,PI/2.[
proof
for x be Real st x in ].0,PI/2.[ holds diff(cosec,x) < 0
proof
let x be Real;
assume
A2: x in ].0,PI/2.[;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;
then sin.x > 0 by A2,COMPTRIG:23;then
A3: (sin.x)^2 > 0 by SQUARE_1:74;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x > 0 by A2,COMPTRIG:27;
then cos.x/(sin.x)^2 > 0/(sin.x)^2 by A3,REAL_1:73;
then -cos.x/(sin.x)^2 < -0 by XREAL_1:26;
hence thesis by A2,Th8;
end;
hence thesis by Th8,COMPTRIG:21,ROLLE:10;
end;
theorem Th17:
sec is_increasing_on [.0,PI/2.[
proof
let r1,r2 be Real;
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 [.0,PI/2.[ & r1 in dom sec & r2 in [.0,PI/2.[ & r2 in dom sec
by A1,A2,XBOOLE_0:def 3;then
A5: 0 <= r1 & r1 < PI/2 & 0 <= r2 & r2 < PI/2 by RCOMP_2:3;
now per cases by A5,REAL_1:def 5;
suppose
A6: 0 = r1;
PI in ].0,4.[ by SIN_COS:def 32;then
A7: PI > 0 by RCOMP_1:47;
A8: sec.r1 = 1/1 by A4,A6,RFUNCT_1:def 8,SIN_COS:33
.= 1;
A9: -PI/2 < r2 & r2 < PI/2 by A4,Lm1,RCOMP_1:47;
-PI/2+2*PI*0 < r2 & r2 < PI/2+2*PI*0 by A4,Lm1,RCOMP_1:47;then
cos r2 > 0 by SIN_COS6:13;then
A10: cos.r2 > 0 by SIN_COS:def 23;
PI/2 < 2*PI by A7,XREAL_1:70;
then r2 < 2*PI by A9,XXREAL_0:2;
then cos r2 < 1 by A3,A6,SIN_COS6:34;
then cos.r2 < 1 by SIN_COS:def 23;
then 1/1 < 1/cos.r2 by A10,XREAL_1:78;
hence sec.r2 > sec.r1 by A4,A8,RFUNCT_1:def 8;
end;
suppose
A13: 0 < r1;
then r1 in ].0,PI/2.[ by A5,RCOMP_1:47;then
A14: r1 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 3;
0 < r2 by A3,A13,XXREAL_0:2;
then r2 in ].0,PI/2.[ by A5,RCOMP_1:47;
then r2 in ].0,PI/2.[ /\ dom sec by A4,XBOOLE_0:def 3;
hence sec.r2 > sec.r1 by A3,A14,Th13,RFUNCT_2:def 2;
end;
end;
hence sec.r2 > sec.r1;
end;
theorem Th18:
sec is_increasing_on ].PI/2,PI.]
proof
let r1,r2 be Real;
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 ].PI/2,PI.] & r1 in dom sec & r2 in ].PI/2,PI.] & r2 in dom sec
by A1,A2,XBOOLE_0:def 3;then
A5: PI/2 < r1 & r1 <= PI & PI/2 < r2 & r2 <= PI by RCOMP_2:4;
now per cases by A5,REAL_1:def 5;
suppose
A6: r2 < PI;
then r1 < PI by A3,XXREAL_0:2;
then r1 in ].PI/2,PI.[ by A5,RCOMP_1:47;then
A7: r1 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 3;
r2 in ].PI/2,PI.[ by A5,A6,RCOMP_1:47;
then r2 in ].PI/2,PI.[ /\ dom sec by A4,XBOOLE_0:def 3;
hence sec.r2 > sec.r1 by A3,A7,Th14,RFUNCT_2:def 2;
end;
suppose
A8: r2 = PI;
A9: sec.r2 = 1/(-1) by A4,A8,RFUNCT_1:def 8,SIN_COS:81
.= -1;
PI in ].0,4.[ by SIN_COS:def 32;then
A10: PI > 0 by RCOMP_1:47;
then PI*1 < PI*(3/2) by XREAL_1:70;
then PI/2+2*PI*0 < r1 & r1 < 3/2*PI+2*PI*0
by A3,A4,A8,RCOMP_2:4,XXREAL_0:2;
then cos r1 < 0 by SIN_COS6:14;then
A11: cos.r1 < 0 by SIN_COS:def 23;
PI/2 > 0/2 by A10,XREAL_1:76;
then r1 > 0 & r1 < PI by A3,A5,XXREAL_0:2;
then cos r1 > -1 by SIN_COS6:35;
then cos.r1 > -1 by SIN_COS:def 23;
then (cos.r1)" < (-1)" by A11,XREAL_1:89;
hence sec.r1 < sec.r2 by A4,A9,RFUNCT_1:def 8;
end;
end;
hence sec.r2 > sec.r1;
end;
theorem Th19:
cosec is_decreasing_on [.-PI/2,0.[
proof
let r1,r2 be Real;
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 [.-PI/2,0.[ & r1 in dom cosec & r2 in [.-PI/2,0.[ & r2 in dom cosec
by A1,A2,XBOOLE_0:def 3;then
A5: -PI/2 <= r1 & r1 < 0 & -PI/2 <= r2 & r2 < 0 by RCOMP_2:3;
now per cases by A5,REAL_1:def 5;
suppose
A6: -PI/2 = r1;
A7: cosec.r1 = 1/sin.(-PI/2) by A4,A6,RFUNCT_1:def 8
.= 1/(-1) by SIN_COS:33,SIN_COS:81
.= -1;
A8: r2 in ].-PI/2,0.[ by A3,A5,A6,RCOMP_1:47;
-PI/2 > -PI by COMPTRIG:21,XREAL_1:26;
then ].-PI/2,0.[ c= ].-PI,0.[ by RCOMP_1:52;
then -PI < r2 & r2 < 0 by A8,RCOMP_1:47;
then -PI+2*PI < r2+2*PI & r2+2*PI < 0+2*PI by XREAL_1:10;
then r2+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(r2+2*PI) < 0 by COMPTRIG:25;then
A9: sin.r2 < 0 by SIN_COS:83;
3/2*PI+2*PI*(-1) < r2 & r2 < 2*PI+2*PI*(-1)
by A3,A4,A6,RCOMP_2:3;
then sin r2 > -1 by SIN_COS6:39;
then sin.r2 > -1 by SIN_COS:def 21;
then (sin.r2)" < (-1)" by A9,XREAL_1:89;
hence cosec.r2 < cosec.r1 by A4,A7,RFUNCT_1:def 8;
end;
suppose
A10: -PI/2 < r1;
then r1 in ].-PI/2,0.[ by A5,RCOMP_1:47;then
A11: r1 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 3;
-PI/2 < r2 by A3,A10,XXREAL_0:2;
then r2 in ].-PI/2,0.[ by A5,RCOMP_1:47;
then r2 in ].-PI/2,0.[ /\ dom cosec by A4,XBOOLE_0:def 3;
hence cosec.r2 < cosec.r1 by A3,A11,Th15,RFUNCT_2:def 3;
end;
end;
hence cosec.r2 < cosec.r1;
end;
theorem Th20:
cosec is_decreasing_on ].0,PI/2.]
proof
let r1,r2 be Real;
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 ].0,PI/2.] & r1 in dom cosec & r2 in ].0,PI/2.] & r2 in dom cosec
by A1,A2,XBOOLE_0:def 3;then
A5: 0 < r1 & r1 <= PI/2 & 0 < r2 & r2 <= PI/2 by RCOMP_2:4;
now per cases by A5,REAL_1:def 5;
suppose
A6: r2 < PI/2;
then r1 < PI/2 by A3,XXREAL_0:2;
then r1 in ].0,PI/2.[ by A5,RCOMP_1:47;then
A7: r1 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 3;
r2 in ].0,PI/2.[ by A5,A6,RCOMP_1:47;
then r2 in ].0,PI/2.[ /\ dom cosec by A4,XBOOLE_0:def 3;
hence cosec.r2 < cosec.r1 by A3,A7,Th16,RFUNCT_2:def 3;
end;
suppose
A8: r2 = PI/2;
A9: cosec.r2 = 1/1 by A4,A8,RFUNCT_1:def 8,SIN_COS:81
.= 1;
A10: sin.r1 > 0 by A4,Lm4,COMPTRIG:23;
sin r1 < 1 by A3,A5,A8,SIN_COS6:30;
then sin.r1 < 1 by SIN_COS:def 21;
then 1/1 < 1/sin.r1 by A10,XREAL_1:78;
hence cosec.r2 < cosec.r1 by A4,A9,RFUNCT_1:def 8;
end;
end;
hence cosec.r2 < cosec.r1;
end;
theorem
sec | [.0,PI/2.[ is one-to-one by Th17,FCONT_3:16;
theorem
sec | ].PI/2,PI.] is one-to-one by Th18,FCONT_3:16;
theorem
cosec | [.-PI/2,0.[ is one-to-one by Th19,FCONT_3:16;
theorem
cosec | ].0,PI/2.] is one-to-one by Th20,FCONT_3:16;
registration
cluster sec | [.0,PI/2.[ -> one-to-one;
coherence by Th17,FCONT_3:16;
cluster sec | ].PI/2,PI.] -> one-to-one;
coherence by Th18,FCONT_3:16;
cluster cosec | [.-PI/2,0.[ -> one-to-one;
coherence by Th19,FCONT_3:16;
cluster cosec | ].0,PI/2.] -> one-to-one;
coherence by Th20,FCONT_3:16;
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 equals
arcsec1.r;
coherence;
func arcsec2 r equals
arcsec2.r;
coherence;
func arccosec1 r equals
arccosec1.r;
coherence;
func arccosec2 r equals
arccosec2.r;
coherence;
end;
definition let r be Real;
redefine func arcsec1 r -> Real;
coherence;
redefine func arcsec2 r -> Real;
coherence;
redefine func arccosec1 r -> Real;
coherence;
redefine func arccosec2 r -> Real;
coherence;
end;
Lm5:
(arcsec1 qua Function)" = sec | [.0,PI/2.[ by FUNCT_1:65;
Lm6:
(arcsec2 qua Function)" = sec | ].PI/2,PI.] by FUNCT_1:65;
Lm7:
(arccosec1 qua Function)" = cosec | [.-PI/2,0.[ by FUNCT_1:65;
Lm8:
(arccosec2 qua Function)" = cosec | ].0,PI/2.] by FUNCT_1:65;
theorem Th25:
rng arcsec1 = [.0,PI/2.[
proof
dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:91;
hence thesis by FUNCT_1:55;
end;
theorem Th26:
rng arcsec2 = ].PI/2,PI.]
proof
dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:91;
hence thesis by FUNCT_1:55;
end;
theorem Th27:
rng arccosec1 = [.-PI/2,0.[
proof
dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:91;
hence thesis by FUNCT_1:55;
end;
theorem Th28:
rng arccosec2 = ].0,PI/2.]
proof
dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:91;
hence thesis by FUNCT_1:55;
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;
definition let th be real number;
redefine func sec th -> Real;
coherence;
redefine func cosec th -> Real;
coherence;
end;
Lm9:
0 in [.0,PI/2.[ & PI/4 in [.0,PI/2.[
proof
A3: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
hence thesis by A3,COMPTRIG:21;
end;
Lm10:
3/4*PI in ].PI/2,PI.] & PI in ].PI/2,PI.]
proof
PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
A2: PI/4+PI/2 > 0+PI/2 by XREAL_1:10;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
PI/4+PI/2 < PI/2+PI/2 by XREAL_1:10;
hence thesis by A2,COMPTRIG:21;
end;
Lm11:
-PI/2 in [.-PI/2,0.[ & -PI/4 in [.-PI/2,0.[
proof
A3: -PI/4 < -0 by XREAL_1:26;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
then -PI/4 > -PI/2 by XREAL_1:26;
hence thesis by A3,COMPTRIG:21;
end;
Lm12:
PI/4 in ].0,PI/2.] & PI/2 in ].0,PI/2.]
proof
A2: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
hence thesis by A2,COMPTRIG:21;
end;
theorem Th29:
sin(PI/4) = 1/sqrt 2 & cos(PI/4) = 1/sqrt 2
proof
A1: 1 = (sin.(PI/4))^2 + (sin.(PI/4))^2 by SIN_COS:31,SIN_COS:78
.= 2*(sin.(PI/4))^2;
(sqrt(1/2))^2 = 1/2 by SQUARE_1:def 4;then
A2: sin.(PI/4) = sqrt(1/2) or sin.(PI/4) = -sqrt(1/2) by A1,SQUARE_1:109;
A4: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
PI/4 < PI/1 by COMPTRIG:21,REAL_2:200;then
A5: PI/4 in ].0,PI.[ by A4,RCOMP_1:47;
sqrt(1/2) > 0 by SQUARE_1:93;then
-sqrt(1/2) <= -0 by XREAL_1:26;
hence thesis by A2,A5,COMPTRIG:23,SQUARE_1:101,SIN_COS:78;
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: sin.(-PI/4) = -1/sqrt 2 by Th29,SIN_COS:33;
A2: cos.(-PI/4) = 1/sqrt 2 by Th29,SIN_COS:33;
A3: sin.(3/4*PI) = sin.(PI+(-PI/4))
.= -(-1/sqrt 2) by A1,SIN_COS:83
.= 1/sqrt 2;
cos.(3/4*PI) = cos.(PI+(-PI/4))
.= -1/sqrt 2 by A2,SIN_COS:83;
hence thesis by A3,Th29,SIN_COS:33;
end;
theorem Th31:
sec 0 = 1 & sec(PI/4) = sqrt 2 &
sec(3/4*PI) = -sqrt 2 & sec PI = -1
proof
A2: sec.0 = 1/1 by Lm9,Th1,RFUNCT_1:def 8,SIN_COS:33
.= 1;
A4: sec.(PI/4) = 1/(1/sqrt 2) by Lm9,Th1,RFUNCT_1:def 8,Th29
.= sqrt 2;
A6: sec.(3/4*PI) = 1/(-1/sqrt 2) by Lm10,Th2,Th30,RFUNCT_1:def 8
.= -1/(1/sqrt 2) by XCMPLX_1:189
.= -sqrt 2;
sec.PI = 1/(-1) by Lm10,Th2,RFUNCT_1:def 8,SIN_COS:81
.= -1;
hence thesis by A2,A4,A6;
end;
theorem Th32:
cosec(-PI/2) = -1 & cosec(-PI/4) = -sqrt 2 &
cosec(PI/4) = sqrt 2 & cosec(PI/2) = 1
proof
A2: cosec.(-PI/2) = 1/sin.(-PI/2) by Lm11,Th3,RFUNCT_1:def 8
.= 1/(-1) by SIN_COS:33,SIN_COS:81
.= -1;
A4: cosec.(-PI/4) = 1/(-1/sqrt 2) by Lm11,Th3,Th30,RFUNCT_1:def 8
.= -1/(1/sqrt 2) by XCMPLX_1:189
.= -sqrt 2;
A6: cosec.(PI/4) = 1/(1/sqrt 2) by Lm12,Th4,Th29,RFUNCT_1:def 8
.= sqrt 2;
cosec.(PI/2) = 1/1 by Lm12,Th4,RFUNCT_1:def 8,SIN_COS:81
.= 1;
hence thesis by A2,A4,A6;
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
A1: x in [.0,PI/4.];
A3: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
then x in ].0,PI/4.[ \/ {0,PI/4} by A1,RCOMP_1:11;then
A4: x in ].0,PI/4.[ or x in {0,PI/4} by XBOOLE_0:def 2;
per cases by A4,TARSKI:def 2;
suppose
A5: x in ].0,PI/4.[;
A6: 0 in [.0,PI/2.[ by COMPTRIG:21;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
AA: PI/4 in [.0,PI/2.[ by A3;then
A7: [.0,PI/4.] c= [.0,PI/2.[ by A6,RCOMP_2:18;
A8: sec is_increasing_on [.0,PI/4.]
by A6,AA,Th17,RCOMP_2:18,RFUNCT_2:60;
A9: 0 in [.0,PI/4.] by A3,RCOMP_1:48;
A10: [.0,PI/4.] /\ dom sec = [.0,PI/4.]
by A7,Th1,XBOOLE_1:1,XBOOLE_1:28;
A11: ].0,PI/4.[ c= [.0,PI/4.] by RCOMP_1:15;
x in { s where s is Real: 0 < s & s < PI/4 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & 0 < s & s < PI/4;then
A12: 1 < sec.x by A5,A8,A9,A10,A11,Th31,RFUNCT_2:def 2;
PI/4 in {s where s is Real: 0 <= s & s <= PI/4} by A3;then
A13: PI/4 in [.0,PI/4.] /\ dom sec by A10,RCOMP_1:def 1;
x in { s where s is Real: 0 < s & s < PI/4 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & 0 < s & s < PI/4;
then sec.x < sqrt 2 by A5,A8,A10,A11,A13,Th31,RFUNCT_2:def 2;then
A14: sec.x in ].1,sqrt 2.[ by A12,RCOMP_1:47;
].1,sqrt 2.[ c= [.1,sqrt 2.] by RCOMP_1:15;
hence sec.x in [.1,sqrt 2.] by A14;
end;
suppose x = 0;
hence sec.x in [.1,sqrt 2.] by Th31,SQUARE_1:84,RCOMP_1:48;
end;
suppose x = PI/4;
hence sec.x in [.1,sqrt 2.] by Th31,SQUARE_1:84,RCOMP_1:48;
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;
assume
A1: x in [.3/4*PI,PI.];
A3: PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A4: PI/4+PI/2 < PI/2+PI/2 by XREAL_1:10;
then x in ].3/4*PI,PI.[ \/ {3/4*PI,PI} by A1,RCOMP_1:11;then
A5: x in ].3/4*PI,PI.[ or x in {3/4*PI,PI} by XBOOLE_0:def 2;
per cases by A5,TARSKI:def 2;
suppose
A6: x in ].3/4*PI,PI.[;
PI/4+PI/4 < PI/2+PI/4 by A3,XREAL_1:10;then
A7: 3/4*PI in ].PI/2,PI.] by A4;
AA: PI in ].PI/2,PI.] by COMPTRIG:21;then
A8: [.3/4*PI,PI.] c= ].PI/2,PI.] by A7,RCOMP_2:19;
A9: sec is_increasing_on [.3/4*PI,PI.]
by A7,AA,Th18,RCOMP_2:19,RFUNCT_2:60;
A10: 3/4*PI in [.3/4*PI,PI.] by A4,RCOMP_1:48;
A11: [.3/4*PI,PI.] /\ dom sec = [.3/4*PI,PI.]
by A8,Th2,XBOOLE_1:1,XBOOLE_1:28;
A12: ].3/4*PI,PI.[ c= [.3/4*PI,PI.] by RCOMP_1:15;
x in { s where s is Real: 3/4*PI < s & s < PI }
by A6,RCOMP_1:def 2;
then ex s be Real st s=x & 3/4*PI < s & s < PI;then
A13: -sqrt 2 < sec.x by A6,A9,A10,A11,A12,Th31,RFUNCT_2:def 2;
PI in {s where s is Real: 3/4*PI <= s & s <= PI} by A4;then
A14: PI in [.3/4*PI,PI.] /\ dom sec by A11,RCOMP_1:def 1;
x in { s where s is Real: 3/4*PI < s & s < PI }
by A6,RCOMP_1:def 2;
then ex s be Real st s=x & 3/4*PI < s & s < PI;
then sec.x < -1 by A6,A9,A11,A12,A14,Th31,RFUNCT_2:def 2;then
A15: sec.x in ].-sqrt 2,-1.[ by A13,RCOMP_1:47;
].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by RCOMP_1:15;
hence sec.x in [.-sqrt 2,-1.] by A15;
end;
suppose
A16: x = 3/4*PI;
-sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
hence sec.x in [.-sqrt 2,-1.] by A16,Th31,RCOMP_1:48;
end;
suppose
A17: x = PI;
-sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
hence sec.x in [.-sqrt 2,-1.] by A17,Th31,RCOMP_1:48;
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;
assume
A1: x in [.-PI/2,-PI/4.];
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A3: -PI/2 < -PI/4 by XREAL_1:26;
then x in ].-PI/2,-PI/4.[ \/ {-PI/2,-PI/4} by A1,RCOMP_1:11;then
A4: x in ].-PI/2,-PI/4.[ or x in {-PI/2,-PI/4} by XBOOLE_0:def 2;
per cases by A4,TARSKI:def 2;
suppose
A5: x in ].-PI/2,-PI/4.[;
A6: -PI/2 in [.-PI/2,0.[ by COMPTRIG:21;
-PI/4 < -0 by XREAL_1:26;then
AA: -PI/4 in [.-PI/2,0.[ by A3;then
A7: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by A6,RCOMP_2:18;
A8: cosec is_decreasing_on [.-PI/2,-PI/4.]
by A6,AA,Th19,RCOMP_2:18,RFUNCT_2:61;
A9: -PI/2 in [.-PI/2,-PI/4.] by A3,RCOMP_1:48;
A10: [.-PI/2,-PI/4.] /\ dom cosec = [.-PI/2,-PI/4.]
by A7,Th3,XBOOLE_1:1,XBOOLE_1:28;
A11: ].-PI/2,-PI/4.[ c= [.-PI/2,-PI/4.] by RCOMP_1:15;
x in { s where s is Real: -PI/2 < s & s < -PI/4 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & -PI/2 < s & s < -PI/4;then
A12: -1 > cosec.x by A5,A8,A9,A10,A11,Th32,RFUNCT_2:def 3;
-PI/4 in {s where s is Real: -PI/2 <= s & s <= -PI/4} by A3;then
A13: -PI/4 in [.-PI/2,-PI/4.] /\ dom cosec by A10,RCOMP_1:def 1;
x in { s where s is Real: -PI/2 < s & s < -PI/4 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & -PI/2 < s & s < -PI/4;
then cosec.x > -sqrt 2 by A5,A8,A10,A11,A13,Th32,RFUNCT_2:def 3;then
A14: cosec.x in ].-sqrt 2,-1.[ by A12,RCOMP_1:47;
].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by RCOMP_1:15;
hence cosec.x in [.-sqrt 2,-1.] by A14;
end;
suppose
A15: x = -PI/2;
-sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
hence cosec.x in [.-sqrt 2,-1.] by A15,Th32,RCOMP_1:48;
end;
suppose
A16: x = -PI/4;
-sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
hence cosec.x in [.-sqrt 2,-1.] by A16,Th32,RCOMP_1:48;
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;
assume
A1: x in [.PI/4,PI/2.];
A3: PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;
then x in ].PI/4,PI/2.[ \/ {PI/4,PI/2} by A1,RCOMP_1:11;then
A4: x in ].PI/4,PI/2.[ or x in {PI/4,PI/2} by XBOOLE_0:def 2;
per cases by A4,TARSKI:def 2;
suppose
A5: x in ].PI/4,PI/2.[;
PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
A6: PI/4 in ].0,PI/2.] by A3;
AA: PI/2 in ].0,PI/2.] by COMPTRIG:21;then
A7: [.PI/4,PI/2.] c= ].0,PI/2.] by A6,RCOMP_2:19;
A8: cosec is_decreasing_on [.PI/4,PI/2.]
by A6,AA,Th20,RCOMP_2:19,RFUNCT_2:61;
A9: PI/4 in [.PI/4,PI/2.] by A3,RCOMP_1:48;
A10: [.PI/4,PI/2.] /\ dom cosec = [.PI/4,PI/2.]
by A7,Th4,XBOOLE_1:1,XBOOLE_1:28;
A11: ].PI/4,PI/2.[ c= [.PI/4,PI/2.] by RCOMP_1:15;
x in { s where s is Real: PI/4 < s & s < PI/2 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & PI/4 < s & s < PI/2;then
A12: sqrt 2 > cosec.x by A5,A8,A9,A10,A11,Th3 2,RFUNCT_2:def 3;
PI/2 in {s where s is Real: PI/4 <= s & s <= PI/2} by A3;then
A13: PI/2 in [.PI/4,PI/2.] /\ dom cosec by A10,RCOMP_1:def 1;
x in { s where s is Real: PI/4 < s & s < PI/2 }
by A5,RCOMP_1:def 2;
then ex s be Real st s=x & PI/4 < s & s < PI/2;
then cosec.x > 1 by A5,A8,A10,A11,A13,Th32,RFUNCT_2:def 3;then
A14: cosec.x in ].1,sqrt 2.[ by A12,RCOMP_1:47;
].1,sqrt 2.[ c= [.1,sqrt 2.] by RCOMP_1:15;
hence cosec.x in [.1,sqrt 2.] by A14;
end;
suppose x = PI/4;
hence cosec.x in [.1,sqrt 2.] by Th32,SQUARE_1:84,RCOMP_1:48;
end;
suppose x = PI/2;
hence cosec.x in [.1,sqrt 2.] by Th32,SQUARE_1:84,RCOMP_1:48;
end;
end;
Lm13:
dom (sec | [.0,PI/4.]) = [.0,PI/4.]
proof
[.0,PI/4.] c= [.0,PI/2.[ by Lm9,RCOMP_2:18;
hence thesis by Th1,XBOOLE_1:1,RELAT_1:91;
end;
Lm14:
dom (sec | [.3/4*PI,PI.]) = [.3/4*PI,PI.]
proof
[.3/4*PI,PI.] c= ].PI/2,PI.] by Lm10,RCOMP_2:19;
hence thesis by Th2,XBOOLE_1:1,RELAT_1:91;
end;
Lm15:
dom (cosec | [.-PI/2,-PI/4.]) = [.-PI/2,-PI/4.]
proof
[.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm11,RCOMP_2:18;
hence thesis by Th3,XBOOLE_1:1,RELAT_1:91;
end;
Lm16:
dom (cosec | [.PI/4,PI/2.]) = [.PI/4,PI/2.]
proof
[.PI/4,PI/2.] c= ].0,PI/2.] by Lm12,RCOMP_2:19;
hence thesis by Th4,XBOOLE_1:1,RELAT_1:91;
end;
Lm17:
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:90;
then dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,XBOOLE_1:28;
hence thesis by FUNCT_1:68;
end;
Lm18:
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:90;
then dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,XBOOLE_1:28;
hence thesis by FUNCT_1:68;
end;
Lm19:
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:90;
then dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,XBOOLE_1:28;
hence thesis by FUNCT_1:68;
end;
Lm20:
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:90;
then dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,XBOOLE_1:28;
hence thesis by FUNCT_1:68;
end;
theorem Th37:
sec is_continuous_on [.0,PI/2.[
proof
for th be real number st th in [.0,PI/2.[ holds
sec|[.0,PI/2.[ is_continuous_in th
proof
let th be real number such that
A0: th in [.0,PI/2.[;
A1: cos.th <> 0 by A0,Lm1,COMPTRIG:27;
AA: cos is_differentiable_in th by SIN_COS:68;
A2: sec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
th in dom (sec|[.0,PI/2.[) &
for rseq st rng rseq c= dom (sec|[.0,PI/2.[) &
rseq is convergent & lim rseq = th holds
(sec|[.0,PI/2.[)*rseq is convergent &
(sec|[.0,PI/2.[).th = lim((sec|[.0,PI/2.[)*rseq)
proof
now let rseq;
assume
A3: rng rseq c= dom (sec|[.0,PI/2.[) &
rseq is convergent & lim rseq = th;
A4: dom (sec|[.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:91;then
rng rseq c= dom sec by A3,Th1,XBOOLE_1:1;then
A6: sec*rseq is convergent & sec.th = lim(sec*rseq)
by A2,A3,FCONT_1:def 1;
(sec|[.0,PI/2.[)*rseq = sec*rseq
proof
now let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:3;
then rseq.n in rng rseq by FUNCT_1:def 5;then
A7: (sec|[.0,PI/2.[).(rseq.n) = sec.(rseq.n) by A3,A4,FUNCT_1:72;
(sec|[.0,PI/2.[).(rseq.n) = ((sec|[.0,PI/2.[)*rseq).n
by A3,RFUNCT_2:21;
hence ((sec|[.0,PI/2.[)*rseq).n = (sec*rseq).n
by A3,A4,A7,Th1,XBOOLE_1:1,RFUNCT_2:21;
end;
hence thesis by FUNCT_2:113;
end;
hence (sec|[.0,PI/2.[)*rseq is convergent &
(sec|[.0,PI/2.[).th = lim((sec|[.0,PI/2.[)*rseq) by A0,A6,Lm17;
end;
hence thesis by A0,Lm17;
end;
hence thesis by FCONT_1:def 1;
end;
hence sec is_continuous_on [.0,PI/2.[ by Th1,FCONT_1:def 2;
end;
theorem Th38:
sec is_continuous_on ].PI/2,PI.]
proof
for th be real number st th in ].PI/2,PI.] holds
sec|].PI/2,PI.] is_continuous_in th
proof
let th be real number such that
A0: th in ].PI/2,PI.];
A1: cos.th <> 0 by A0,Lm2,COMPTRIG:29;
AA: cos is_differentiable_in th by SIN_COS:68;
A2: sec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
th in dom (sec|].PI/2,PI.]) &
for rseq st rng rseq c= dom (sec|].PI/2,PI.]) &
rseq is convergent & lim rseq = th holds
(sec|].PI/2,PI.])*rseq is convergent &
(sec|].PI/2,PI.]).th = lim((sec|].PI/2,PI.])*rseq)
proof
now let rseq;
assume
A3: rng rseq c= dom (sec|].PI/2,PI.]) &
rseq is convergent & lim rseq = th;
A4: dom (sec|].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:91;then
rng rseq c= dom sec by A3,Th2,XBOOLE_1:1;then
A6: sec*rseq is convergent & sec.th = lim(sec*rseq)
by A2,A3,FCONT_1:def 1;
(sec|].PI/2,PI.])*rseq = sec*rseq
proof
now let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:3;
then rseq.n in rng rseq by FUNCT_1:def 5;then
A7: (sec|].PI/2,PI.]).(rseq.n) = sec.(rseq.n)
by A3,A4,FUNCT_1:72;
(sec|].PI/2,PI.]).(rseq.n) = ((sec|].PI/2,PI.])*rseq).n
by A3,RFUNCT_2:21;
hence ((sec|].PI/2,PI.])*rseq).n = (sec*rseq).n
by A3,A4,A7,Th2,XBOOLE_1:1,RFUNCT_2:21;
end;
hence thesis by FUNCT_2:113;
end;
hence (sec|].PI/2,PI.])*rseq is convergent &
(sec|].PI/2,PI.]).th = lim((sec|].PI/2,PI.])*rseq) by A0,A6,Lm18;
end;
hence thesis by A0,Lm18;
end;
hence thesis by FCONT_1:def 1;
end;
hence sec is_continuous_on ].PI/2,PI.] by Th2,FCONT_1:def 2;
end;
theorem Th39:
cosec is_continuous_on [.-PI/2,0.[
proof
for th be real number st th in [.-PI/2,0.[ holds
cosec|[.-PI/2,0.[ is_continuous_in th
proof
let th be real number such that
A0: th in [.-PI/2,0.[;
-PI < th & th < 0 by A0,Lm3,RCOMP_1:47;
then -PI+2*PI < th+2*PI & th+2*PI < 0+2*PI by XREAL_1:10;
then th+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(th+2*PI) <> 0 by COMPTRIG:25;then
A1: sin.th <> 0 by SIN_COS:83;
AA: sin is_differentiable_in th by SIN_COS:69;
A2: cosec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
th in dom (cosec|[.-PI/2,0.[) &
for rseq st rng rseq c= dom (cosec|[.-PI/2,0.[) &
rseq is convergent & lim rseq = th holds
(cosec|[.-PI/2,0.[)*rseq is convergent &
(cosec|[.-PI/2,0.[).th = lim((cosec|[.-PI/2,0.[)*rseq)
proof
now let rseq;
assume
A3: rng rseq c= dom (cosec|[.-PI/2,0.[) &
rseq is convergent & lim rseq = th;
A4: dom (cosec|[.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:91;then
rng rseq c= dom cosec by A3,Th3,XBOOLE_1:1;then
A6: cosec*rseq is convergent & cosec.th = lim(cosec*rseq)
by A2,A3,FCONT_1:def 1;
(cosec|[.-PI/2,0.[)*rseq = cosec*rseq
proof
now let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:3;
then rseq.n in rng rseq by FUNCT_1:def 5;then
A7: (cosec|[.-PI/2,0.[).(rseq.n) = cosec.(rseq.n)
by A3,A4,FUNCT_1:72;
(cosec|[.-PI/2,0.[).(rseq.n) = ((cosec|[.-PI/2,0.[)*rseq).n
by A3,RFUNCT_2:21;
hence ((cosec|[.-PI/2,0.[)*rseq).n = (cosec*rseq).n
by A3,A4,A7,Th3,XBOOLE_1:1,RFUNCT_2:21;
end;
hence thesis by FUNCT_2:113;
end;
hence (cosec|[.-PI/2,0.[)*rseq is convergent &
(cosec|[.-PI/2,0.[).th = lim((cosec|[.-PI/2,0.[)*rseq)
by A0,A6,Lm19;
end;
hence thesis by A0,Lm19;
end;
hence thesis by FCONT_1:def 1;
end;
hence cosec is_continuous_on [.-PI/2,0.[ by Th3,FCONT_1:def 2;
end;
theorem Th40:
cosec is_continuous_on ].0,PI/2.]
proof
for th be real number st th in ].0,PI/2.] holds
cosec|].0,PI/2.] is_continuous_in th
proof
let th be real number such that
A0: th in ].0,PI/2.];
A1: sin.th <> 0 by A0,Lm4,COMPTRIG:23;
AA: sin is_differentiable_in th by SIN_COS:69;
A2: cosec is_continuous_in th by A1,AA,FDIFF_1:32,FCONT_1:10;
th in dom (cosec|].0,PI/2.]) &
for rseq st rng rseq c= dom (cosec|].0,PI/2.]) &
rseq is convergent & lim rseq = th holds
(cosec|].0,PI/2.])*rseq is convergent &
(cosec|].0,PI/2.]).th = lim((cosec|].0,PI/2.])*rseq)
proof
now let rseq;
assume
A3: rng rseq c= dom (cosec|].0,PI/2.]) &
rseq is convergent & lim rseq = th;
A4: dom (cosec|].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:91;then
rng rseq c= dom cosec by A3,Th4,XBOOLE_1:1;then
A6: cosec*rseq is convergent & cosec.th = lim(cosec*rseq)
by A2,A3,FCONT_1:def 1;
(cosec|].0,PI/2.])*rseq = cosec*rseq
proof
now let n be Element of NAT;
dom (rseq) = NAT by SEQ_1:3;
then rseq.n in rng rseq by FUNCT_1:def 5;then
A7: (cosec|].0,PI/2.]).(rseq.n) = cosec.(rseq.n)
by A3,A4,FUNCT_1:72;
(cosec|].0,PI/2.]).(rseq.n) = ((cosec|].0,PI/2.])*rseq).n
by A3,RFUNCT_2:21;
hence ((cosec|].0,PI/2.])*rseq).n = (cosec*rseq).n
by A3,A4,A7,Th4,XBOOLE_1:1,RFUNCT_2:21;
end;
hence thesis by FUNCT_2:113;
end;
hence (cosec|].0,PI/2.])*rseq is convergent &
(cosec|].0,PI/2.]).th = lim((cosec|].0,PI/2.])*rseq)
by A0,A6,Lm20;
end;
hence thesis by A0,Lm20;
end;
hence thesis by FCONT_1:def 1;
end;
hence cosec is_continuous_on ].0,PI/2.] by Th4,FCONT_1:def 2;
end;
theorem Th41:
rng(sec | [.0,PI/4.]) = [.1,sqrt 2.]
proof
now let y be set;
thus y in [.1,sqrt 2.] implies ex x be set
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;
A2: PI/4 >= 0 by Lm9,RCOMP_2:3;
A4: sec is_continuous_on [.0,PI/4.]
by Lm9,Th37,RCOMP_2:18,FCONT_1:17;
y1 in [.sec.0,sec.(PI/4).] \/ [.sec.(PI/4),sec.0.]
by A1,Th31,XBOOLE_0:def 2;
then consider x be Real such that
A5: x in [.0,PI/4.] and
A6: y1 = sec.x by A2,A4,FCONT_2:16;
take x;
thus x in dom (sec | [.0,PI/4.]) & y = (sec | [.0,PI/4.]).x
by A5,A6,Lm13,FUNCT_1:72;
end;
thus (ex x be set st x in dom (sec | [.0,PI/4.]) &
y = (sec | [.0,PI/4.]).x) implies y in [.1,sqrt 2.]
proof
given x be set such that
A7: x in dom (sec | [.0,PI/4.]) and
A8: y = (sec | [.0,PI/4.]).x;
reconsider x1=x as Real by A7;
y = sec.x1 by A7,A8,Lm13,FUNCT_1:72;
hence y in [.1,sqrt 2.] by A7,Lm13,Th33;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th42:
rng(sec | [.3/4*PI,PI.]) = [.-sqrt 2,-1.]
proof
now let y be set;
thus y in [.-sqrt 2,-1.] implies ex x be set
st x in dom (sec | [.3/4*PI,PI.]) & y = (sec | [.3/4*PI,PI.]).x
proof
assume
A1: y in [.-sqrt 2,-1.];
then reconsider y1=y as Real;
A2: 3/4*PI <= PI by Lm10,RCOMP_2:4;
A4: sec is_continuous_on [.3/4*PI,PI.]
by Lm10,Th38,RCOMP_2:19,FCONT_1:17;
y1 in [.sec.(3/4*PI),sec.PI.] \/ [.sec.PI,sec.(3/4*PI).]
by A1,Th31,XBOOLE_0:def 2;
then consider x be Real such that
A5: x in [.3/4*PI,PI.] and
A6: y1 = sec.x by A2,A4,FCONT_2:16;
take x;
thus x in dom (sec | [.3/4*PI,PI.]) & y = (sec | [.3/4*PI,PI.]).x
by A5,A6,Lm14,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A7: x in dom (sec | [.3/4*PI,PI.]) and
A8: y = (sec | [.3/4*PI,PI.]).x;
reconsider x1=x as Real by A7;
y = sec.x1 by A7,A8,Lm14,FUNCT_1:72;
hence y in [.-sqrt 2,-1.] by A7,Lm14,Th34;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th43:
rng(cosec | [.-PI/2,-PI/4.]) = [.-sqrt 2,-1.]
proof
now let y be set;
thus y in [.-sqrt 2,-1.] implies ex x be set
st x in dom (cosec | [.-PI/2,-PI/4.]) & y = (cosec | [.-PI/2,-PI/4.]).x
proof
assume
A1: y in [.-sqrt 2,-1.];
then reconsider y1=y as Real;
A2: -PI/2 <= -PI/4 by Lm11,RCOMP_2:3;
A4: cosec is_continuous_on [.-PI/2,-PI/4.]
by Lm11,Th39,RCOMP_2:18,FCONT_1:17;
y1 in [.cosec.(-PI/4),cosec.(-PI/2).] \/
[.cosec.(-PI/2),cosec.(-PI/4).] by A1,Th32,XBOOLE_0:def 2;
then consider x be Real such that
A5: x in [.-PI/2,-PI/4.] and
A6: y1 = cosec.x by A2,A4,FCONT_2:16;
take x;
thus x in dom (cosec | [.-PI/2,-PI/4.]) &
y = (cosec | [.-PI/2,-PI/4.]).x by A5,A6,Lm15,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A7: x in dom (cosec | [.-PI/2,-PI/4.]) and
A8: y = (cosec | [.-PI/2,-PI/4.]).x;
reconsider x1=x as Real by A7;
y = cosec.x1 by A7,A8,Lm15,FUNCT_1:72;
hence y in [.-sqrt 2,-1.] by A7,Lm15,Th35;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th44:
rng(cosec | [.PI/4,PI/2.]) = [.1,sqrt 2.]
proof
now let y be set;
thus y in [.1,sqrt 2.] implies ex x be set
st x in dom (cosec | [.PI/4,PI/2.]) & y = (cosec | [.PI/4,PI/2.]).x
proof
assume
A1: y in [.1,sqrt 2.];
then reconsider y1=y as Real;
A2: PI/4 <= PI/2 by Lm12,RCOMP_2:4;
A4: cosec is_continuous_on [.PI/4,PI/2.]
by Lm12,Th40,RCOMP_2:19,FCONT_1:17;
y1 in [.cosec.(PI/2),cosec.(PI/4).] \/
[.cosec.(PI/4),cosec.(PI/2).] by A1,Th32,XBOOLE_0:def 2;
then consider x be Real such that
A5: x in [.PI/4,PI/2.] and
A6: y1 = cosec.x by A2,A4,FCONT_2:16;
take x;
thus x in dom (cosec | [.PI/4,PI/2.]) &
y = (cosec | [.PI/4,PI/2.]).x by A5,A6,Lm16,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A7: x in dom (cosec | [.PI/4,PI/2.]) and
A8: y = (cosec | [.PI/4,PI/2.]).x;
reconsider x1=x as Real by A7;
y = cosec.x1 by A7,A8,Lm16,FUNCT_1:72;
hence y in [.1,sqrt 2.] by A7,Lm16,Th36;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th45:
[.1,sqrt 2.] c= dom arcsec1
proof
A1: [.0,PI/4.] c= [.0,PI/2.[ by Lm9,RCOMP_2:18;
A2: rng(sec | [.0,PI/4.]) c= rng(sec | [.0,PI/2.[)
proof
let y be set;
assume y in rng(sec | [.0,PI/4.]);
then y in sec.:[.0,PI/4.] by RELAT_1:148;
then consider x be set such that
A3: x in dom sec and
A4: x in [.0,PI/4.] and
A5: y = sec.x by FUNCT_1:def 12;
y in sec.:[.0,PI/2.[ by A1,A3,A4,A5,FUNCT_1:def 12;
hence thesis by RELAT_1:148;
end;
thus [.1,sqrt 2.] c= dom arcsec1 by A2,Th41,FUNCT_1:55;
end;
theorem Th46:
[.-sqrt 2,-1.] c= dom arcsec2
proof
A1: [.3/4*PI,PI.] c= ].PI/2,PI.] by Lm10,RCOMP_2:19;
A2: rng(sec | [.3/4*PI,PI.]) c= rng(sec | ].PI/2,PI.])
proof
let y be set;
assume y in rng(sec | [.3/4*PI,PI.]);
then y in sec.:[.3/4*PI,PI.] by RELAT_1:148;
then consider x be set such that
A3: x in dom sec and
A4: x in [.3/4*PI,PI.] and
A5: y = sec.x by FUNCT_1:def 12;
y in sec.:].PI/2,PI.] by A1,A3,A4,A5,FUNCT_1:def 12;
hence thesis by RELAT_1:148;
end;
thus [.-sqrt 2,-1.] c= dom arcsec2 by A2,Th42,FUNCT_1:55;
end;
theorem Th47:
[.-sqrt 2,-1.] c= dom arccosec1
proof
A1: [.-PI/2,-PI/4.] c= [.-PI/2,0.[ by Lm11,RCOMP_2:18;
A2: rng(cosec | [.-PI/2,-PI/4.]) c= rng(cosec | [.-PI/2,0.[)
proof
let y be set;
assume y in rng(cosec | [.-PI/2,-PI/4.]);
then y in cosec.:[.-PI/2,-PI/4.] by RELAT_1:148;
then consider x be set such that
A3: x in dom cosec and
A4: x in [.-PI/2,-PI/4.] and
A5: y = cosec.x by FUNCT_1:def 12;
y in cosec.:[.-PI/2,0.[ by A1,A3,A4,A5,FUNCT_1:def 12;
hence thesis by RELAT_1:148;
end;
thus [.-sqrt 2,-1.] c= dom arccosec1 by A2,Th43,FUNCT_1:55;
end;
theorem Th48:
[.1,sqrt 2.] c= dom arccosec2
proof
A1: [.PI/4,PI/2.] c= ].0,PI/2.] by Lm12,RCOMP_2:19;
A2: rng(cosec | [.PI/4,PI/2.]) c= rng(cosec | ].0,PI/2.])
proof
let y be set;
assume y in rng(cosec | [.PI/4,PI/2.]);
then y in cosec.:[.PI/4,PI/2.] by RELAT_1:148;
then consider x be set such that
A3: x in dom cosec and
A4: x in [.PI/4,PI/2.] and
A5: y = cosec.x by FUNCT_1:def 12;
y in cosec.:].0,PI/2.] by A1,A3,A4,A5,FUNCT_1:def 12;
hence thesis by RELAT_1:148;
end;
thus [.1,sqrt 2.] c= dom arccosec2 by A2,Th44,FUNCT_1:55;
end;
Lm21:
sec | [.0,PI/4.] is_increasing_on [.0,PI/4.]
proof
sec is_increasing_on [.0,PI/4.]
by Lm9,Th17,RCOMP_2:18,RFUNCT_2:60;
hence thesis by RFUNCT_2:50;
end;
Lm22:
sec | [.3/4*PI,PI.] is_increasing_on [.3/4*PI,PI.]
proof
sec is_increasing_on [.3/4*PI,PI.]
by Lm10,Th18,RCOMP_2:19,RFUNCT_2:60;
hence thesis by RFUNCT_2:50;
end;
Lm23:
cosec | [.-PI/2,-PI/4.] is_decreasing_on [.-PI/2,-PI/4.]
proof
cosec is_decreasing_on [.-PI/2,-PI/4.]
by Lm11,Th19,RCOMP_2:18,RFUNCT_2:61;
hence thesis by RFUNCT_2:51;
end;
Lm24:
cosec | [.PI/4,PI/2.] is_decreasing_on [.PI/4,PI/2.]
proof
cosec is_decreasing_on [.PI/4,PI/2.]
by Lm12,Th20,RCOMP_2:19,RFUNCT_2:61;
hence thesis by RFUNCT_2:51;
end;
Lm25:
sec | [.0,PI/4.] is one-to-one
proof
(sec | [.0,PI/2.[) | [.0,PI/4.] = sec | [.0,PI/4.]
by Lm9,RCOMP_2:18,RELAT_1:103;
hence sec | [.0,PI/4.] is one-to-one;
end;
Lm26:
sec | [.3/4*PI,PI.] is one-to-one
proof
(sec | ].PI/2,PI.]) | [.3/4*PI,PI.] = sec | [.3/4*PI,PI.]
by Lm10,RCOMP_2:19,RELAT_1:103;
hence sec | [.3/4*PI,PI.] is one-to-one;
end;
Lm27:
cosec | [.-PI/2,-PI/4.] is one-to-one
proof
(cosec | [.-PI/2,0.[) | [.-PI/2,-PI/4.] = cosec | [.-PI/2,-PI/4.]
by Lm11,RCOMP_2:18,RELAT_1:103;
hence cosec | [.-PI/2,-PI/4.] is one-to-one;
end;
Lm28:
cosec | [.PI/4,PI/2.] is one-to-one
proof
(cosec | ].0,PI/2.]) | [.PI/4,PI/2.] = cosec | [.PI/4,PI/2.]
by Lm12,RCOMP_2:19,RELAT_1:103;
hence cosec | [.PI/4,PI/2.] is one-to-one;
end;
registration
cluster sec | [.0,PI/4.] -> one-to-one;
coherence by Lm25;
cluster sec | [.3/4*PI,PI.] -> one-to-one;
coherence by Lm26;
cluster cosec | [.-PI/2,-PI/4.] -> one-to-one;
coherence by Lm27;
cluster cosec | [.PI/4,PI/2.] -> one-to-one;
coherence by Lm28;
end;
theorem Th49:
arcsec1 | [.1,sqrt 2.] = (sec | [.0,PI/4.])"
proof
set h = sec | [.0,PI/2.[;
(sec | [.0,PI/4.])" = (h | [.0,PI/4.])"
by Lm9,RCOMP_2:18,RELAT_1:103
.= h" | (h.:[.0,PI/4.]) by RFUNCT_2:40
.= h" | rng (h | [.0,PI/4.]) by RELAT_1:148
.= h" | ([.1,sqrt 2.]) by Th41,Lm9,RCOMP_2:18,RELAT_1:103;
hence (sec | [.0,PI/4.])" = arcsec1 | [.1,sqrt 2.];
end;
theorem Th50:
arcsec2 | [.-sqrt 2,-1.] = (sec | [.3/4*PI,PI.])"
proof
set h = sec | ].PI/2,PI.];
(sec | [.3/4*PI,PI.])" = (h | [.3/4*PI,PI.])"
by Lm10,RCOMP_2:19,RELAT_1:103
.= h" | (h.:[.3/4*PI,PI.]) by RFUNCT_2:40
.= h" | rng (h | [.3/4*PI,PI.]) by RELAT_1:148
.= h" | ([.-sqrt 2,-1.]) by Th42,Lm10,RCOMP_2:19,RELAT_1:103;
hence (sec | [.3/4*PI,PI.])" = arcsec2 | [.-sqrt 2,-1.];
end;
theorem Th51:
arccosec1 | [.-sqrt 2,-1.] = (cosec | [.-PI/2,-PI/4.])"
proof
set h = cosec | [.-PI/2,0.[;
(cosec | [.-PI/2,-PI/4.])" = (h | [.-PI/2,-PI/4.])"
by Lm11,RCOMP_2:18,RELAT_1:103
.= h" | (h.:[.-PI/2,-PI/4.]) by RFUNCT_2:40
.= h" | rng (h | [.-PI/2,-PI/4.]) by RELAT_1:148
.= h" | ([.-sqrt 2,-1.]) by Th43,Lm11,RCOMP_2:18,RELAT_1:103;
hence (cosec | [.-PI/2,-PI/4.])" = arccosec1 | [.-sqrt 2,-1.];
end;
theorem Th52:
arccosec2 | [.1,sqrt 2.] = (cosec | [.PI/4,PI/2.])"
proof
set h = cosec | ].0,PI/2.];
(cosec | [.PI/4,PI/2.])" = (h | [.PI/4,PI/2.])"
by Lm12,RCOMP_2:19,RELAT_1:103
.= h" | (h.:[.PI/4,PI/2.]) by RFUNCT_2:40
.= h" | rng (h | [.PI/4,PI/2.]) by RELAT_1:148
.= h" | ([.1,sqrt 2.]) by Th44,Lm12,RCOMP_2:19,RELAT_1:103;
hence (cosec | [.PI/4,PI/2.])" = arccosec2 | [.1,sqrt 2.];
end;
theorem
(sec | [.0,PI/4.]) qua Function * (arcsec1 | [.1,sqrt 2.])
= id [.1,sqrt 2.] by Th41,Th49,FUNCT_1:61;
theorem
(sec | [.3/4*PI,PI.]) qua Function * (arcsec2 | [.-sqrt 2,-1.])
= id [.-sqrt 2,-1.] by Th42,Th50,FUNCT_1:61;
theorem
(cosec | [.-PI/2,-PI/4.]) qua Function * (arccosec1 | [.-sqrt 2,-1.])
= id [.-sqrt 2,-1.] by Th43,Th51,FUNCT_1:61;
theorem
(cosec | [.PI/4,PI/2.]) qua Function * (arccosec2 | [.1,sqrt 2.])
= id [.1,sqrt 2.] by Th44,Th52,FUNCT_1:61;
theorem
(sec | [.0,PI/4.]) * (arcsec1 | [.1,sqrt 2.]) = id [.1,sqrt 2.]
by Th41,Th49,FUNCT_1:61;
theorem
(sec | [.3/4*PI,PI.]) * (arcsec2 | [.-sqrt 2,-1.]) = id [.-sqrt 2,-1.]
by Th42,Th50,FUNCT_1:61;
theorem
(cosec | [.-PI/2,-PI/4.]) * (arccosec1 | [.-sqrt 2,-1.])
= id [.-sqrt 2,-1.] by Th43,Th51,FUNCT_1:61;
theorem
(cosec | [.PI/4,PI/2.]) * (arccosec2 | [.1,sqrt 2.])
= id [.1,sqrt 2.] by Th44,Th52,FUNCT_1:61;
theorem
arcsec1 qua Function * (sec | [.0,PI/2.[) = id [.0,PI/2.[
by Lm5,Th25,FUNCT_1:61;
theorem
arcsec2 qua Function * (sec | ].PI/2,PI.]) = id ].PI/2,PI.]
by Lm6,Th26,FUNCT_1:61;
theorem
arccosec1 qua Function * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[
by Lm7,Th27,FUNCT_1:61;
theorem
arccosec2 qua Function * (cosec | ].0,PI/2.]) = id ].0,PI/2.]
by Lm8,Th28,FUNCT_1:61;
theorem Th65:
arcsec1 * (sec | [.0,PI/2.[) = id [.0,PI/2.[ by Lm5,Th25,FUNCT_1:61;
theorem Th66:
arcsec2 * (sec | ].PI/2,PI.]) = id ].PI/2,PI.] by Lm6,Th26,FUNCT_1:61;
theorem Th67:
arccosec1 * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[ by Lm7,Th27,FUNCT_1:61;
theorem Th68:
arccosec2 * (cosec | ].0,PI/2.]) = id ].0,PI/2.] by Lm8,Th28,FUNCT_1:61;
theorem Th69:
0 <= r & r < PI/2 implies arcsec1 sec r = r
proof
assume 0 <= r & r < PI/2;then
A1: r in [.0,PI/2.[;
A2: dom (sec | [.0,PI/2.[) = [.0,PI/2.[ by Th1,RELAT_1:91;
arcsec1 sec.r = arcsec1.((sec|[.0,PI/2.[).r) by A1,FUNCT_1:72
.= (id [.0,PI/2.[).r by A1,A2,Th65,FUNCT_1:23
.= r by A1,FUNCT_1:35;
hence thesis;
end;
theorem Th70:
PI/2 < r & r <= PI implies arcsec2 sec r = r
proof
assume PI/2 < r & r <= PI;then
A1: r in ].PI/2,PI.];
A2: dom (sec | ].PI/2,PI.]) = ].PI/2,PI.] by Th2,RELAT_1:91;
arcsec2 sec.r = arcsec2.((sec|].PI/2,PI.]).r) by A1,FUNCT_1:72
.= (id ].PI/2,PI.]).r by A1,A2,Th66,FUNCT_1:23
.= r by A1,FUNCT_1:35;
hence thesis;
end;
theorem Th71:
-PI/2 <= r & r < 0 implies arccosec1 cosec r = r
proof
assume -PI/2 <= r & r < 0;then
A1: r in [.-PI/2,0.[;
A2: dom (cosec | [.-PI/2,0.[) = [.-PI/2,0.[ by Th3,RELAT_1:91;
arccosec1 cosec.r = arccosec1.((cosec|[.-PI/2,0.[).r) by A1,FUNCT_1:72
.= (id [.-PI/2,0.[).r by A1,A2,Th67,FUNCT_1:23
.= r by A1,FUNCT_1:35;
hence thesis;
end;
theorem Th72:
0 < r & r <= PI/2 implies arccosec2 cosec r = r
proof
assume 0 < r & r <= PI/2;then
A1: r in ].0,PI/2.];
A2: dom (cosec | ].0,PI/2.]) = ].0,PI/2.] by Th4,RELAT_1:91;
arccosec2 cosec.r = arccosec2.((cosec|].0,PI/2.]).r) by A1,FUNCT_1:72
.= (id ].0,PI/2.]).r by A1,A2,Th68,FUNCT_1:23
.= r by A1,FUNCT_1:35;
hence thesis;
end;
theorem Th73:
arcsec1 1 = 0 & arcsec1(sqrt 2) = PI/4
proof
A1: 0 <= 0 & 0 < PI/2 by Lm9,RCOMP_2:3;
A2: arcsec1.1 = arcsec1 1
.= 0 by A1,Th31,Th69;
A3: 0 <= PI/4 & PI/4 < PI/2 by Lm9,RCOMP_2:3;
arcsec1.(sqrt 2) = arcsec1 (sqrt 2)
.= PI/4 by A3,Th31,Th69;
hence thesis by A2;
end;
theorem Th74:
arcsec2(-sqrt 2) = 3/4*PI & arcsec2(-1) = PI
proof
A1: PI/2 < 3/4*PI & 3/4*PI <= PI by Lm10,RCOMP_2:4;
A2: arcsec2.(-sqrt 2) = arcsec2 (-sqrt 2)
.= 3/4*PI by A1,Th31,Th70;
A3: PI/2 < PI & PI <= PI by Lm10,RCOMP_2:4;
arcsec2.(-1) = arcsec2 (-1)
.= PI by A3,Th31,Th70;
hence thesis by A2;
end;
theorem Th75:
arccosec1(-1) = -PI/2 & arccosec1(-sqrt 2) = -PI/4
proof
A1: -PI/2 <= -PI/2 & -PI/2 < 0 by Lm11,RCOMP_2:3;
A2: arccosec1.(-1) = arccosec1 (-1)
.= -PI/2 by A1,Th32,Th71;
A3: -PI/2 <= -PI/4 & -PI/4 < 0 by Lm11,RCOMP_2:3;
arccosec1.(-sqrt 2) = arccosec1 (-sqrt 2)
.= -PI/4 by A3,Th32,Th71;
hence thesis by A2;
end;
theorem Th76:
arccosec2(sqrt 2) = PI/4 & arccosec2 1 = PI/2
proof
A1: 0 < PI/4 & PI/4 <= PI/2 by Lm12,RCOMP_2:4;
A2: arccosec2.(sqrt 2) = arccosec2 (sqrt 2)
.= PI/4 by A1,Th32,Th72;
A3: 0 < PI/2 & PI/2 <= PI/2 by Lm12,RCOMP_2:4;
arccosec2.1 = arccosec2 1
.= PI/2 by A3,Th32,Th72;
hence thesis by A2;
end;
theorem Th77:
arcsec1 is_increasing_on sec.:[.0,PI/2.[
proof
set f = sec | [.0,PI/2.[;
A1: f|[.0,PI/2.[ = f by RELAT_1:102;
A2: f is_increasing_on [.0,PI/2.[ by Th17,RFUNCT_2:50;
f.:[.0,PI/2.[ = rng(f|[.0,PI/2.[) by RELAT_1:148
.= rng(sec|[.0,PI/2.[) by RELAT_1:102
.= sec.:[.0,PI/2.[ by RELAT_1:148;
hence arcsec1 is_increasing_on sec.:[.0,PI/2.[ by A1,A2,FCONT_3:17;
end;
theorem Th78:
arcsec2 is_increasing_on sec.:].PI/2,PI.]
proof
set f = sec | ].PI/2,PI.];
A1: f|].PI/2,PI.] = f by RELAT_1:102;
A2: f is_increasing_on ].PI/2,PI.] by Th18,RFUNCT_2:50;
f.:].PI/2,PI.] = rng(f|].PI/2,PI.]) by RELAT_1:148
.= rng(sec|].PI/2,PI.]) by RELAT_1:102
.= sec.:].PI/2,PI.] by RELAT_1:148;
hence arcsec2 is_increasing_on sec.:].PI/2,PI.] by A1,A2,FCONT_3:17;
end;
theorem Th79:
arccosec1 is_decreasing_on cosec.:[.-PI/2,0.[
proof
set f = cosec | [.-PI/2,0.[;
A1: f|[.-PI/2,0.[ = f by RELAT_1:102;
A2: f is_decreasing_on [.-PI/2,0.[ by Th19,RFUNCT_2:51;
f.:[.-PI/2,0.[ = rng(f|[.-PI/2,0.[) by RELAT_1:148
.= rng(cosec|[.-PI/2,0.[) by RELAT_1:102
.= cosec.:[.-PI/2,0.[ by RELAT_1:148;
hence arccosec1 is_decreasing_on cosec.:[.-PI/2,0.[ by A1,A2,FCONT_3:18;
end;
theorem Th80:
arccosec2 is_decreasing_on cosec.:].0,PI/2.]
proof
set f = cosec | ].0,PI/2.];
A1: f|].0,PI/2.] = f by RELAT_1:102;
A2: f is_decreasing_on ].0,PI/2.] by Th20,RFUNCT_2:51;
f.:].0,PI/2.] = rng(f|].0,PI/2.]) by RELAT_1:148
.= rng(cosec|].0,PI/2.]) by RELAT_1:102
.= cosec.:].0,PI/2.] by RELAT_1:148;
hence arccosec2 is_decreasing_on cosec.:].0,PI/2.] by A1,A2,FCONT_3:18;
end;
theorem Th81:
arcsec1 is_increasing_on [.1,sqrt 2.]
proof
A1: [.1,sqrt 2.] = sec.:[.0,PI/4.] by Th41,RELAT_1:148;
[.1,sqrt 2.] c= sec.:[.0,PI/2.[ by A1,Lm9,RCOMP_2:18,RELAT_1:156;
hence arcsec1 is_increasing_on [.1,sqrt 2.] by Th77,RFUNCT_2:60;
end;
theorem Th82:
arcsec2 is_increasing_on [.-sqrt 2,-1.]
proof
A1: [.-sqrt 2,-1.] = sec.:[.3/4*PI,PI.] by Th42,RELAT_1:148;
[.-sqrt 2,-1.] c= sec.:].PI/2,PI.] by A1,RELAT_1:156,Lm10,RCOMP_2:19;
hence arcsec2 is_increasing_on [.-sqrt 2,-1.] by Th78,RFUNCT_2:60;
end;
theorem Th83:
arccosec1 is_decreasing_on [.-sqrt 2,-1.]
proof
A1: [.-sqrt 2,-1.] = cosec.:[.-PI/2,-PI/4.] by Th43,RELAT_1:148;
[.-sqrt 2,-1.] c= cosec.:[.-PI/2,0.[ by A1,Lm11,RCOMP_2:18,RELAT_1:156;
hence arccosec1 is_decreasing_on [.-sqrt 2,-1.] by Th79,RFUNCT_2:61;
end;
theorem Th84:
arccosec2 is_decreasing_on [.1,sqrt 2.]
proof
A1: [.1,sqrt 2.] = cosec.:[.PI/4,PI/2.] by Th44,RELAT_1:148;
[.1,sqrt 2.] c= cosec.:].0,PI/2.] by A1,Lm12,RCOMP_2:19,RELAT_1:156;
hence arccosec2 is_decreasing_on [.1,sqrt 2.] by Th80,RFUNCT_2:61;
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:84,RCOMP_1:11;then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 2;
per cases by A1,TARSKI:def 2;
suppose
A2: x in ].1,sqrt 2.[;
A3: 1 in [.1,sqrt 2.] by SQUARE_1:84,RCOMP_1:48;
A4: [.1,sqrt 2.] /\ dom arcsec1 = [.1,sqrt 2.] by Th45,XBOOLE_1:28;
A5: ].1,sqrt 2.[ c= [.1,sqrt 2.] by RCOMP_1:15;
x in {s where s is Real: 1 < s & s < sqrt 2} by A2,RCOMP_1:def 2;then
A6: ex s be Real st s=x & 1 < s & s < sqrt 2;then
A7: 0 < arcsec1.x by A2,A3,A4,A5,Th73,Th81,RFUNCT_2:def 2;
sqrt 2 in [.1,sqrt 2.] /\ dom arcsec1 by A4,SQUARE_1:84,RCOMP_1:48;
then arcsec1.x < PI/4 by A2,A4,A5,A6,Th73,Th81,RFUNCT_2:def 2;
hence arcsec1.x in [.0,PI/4.] by A7,RCOMP_1:48;
end;
suppose
A8: x = 1;
0 <= PI/4 by Lm9,RCOMP_2:3;
hence arcsec1.x in [.0,PI/4.] by A8,Th73,RCOMP_1:48;
end;
suppose
A9: x = sqrt 2;
0 <= PI/4 by Lm9,RCOMP_2:3;
hence arcsec1.x in [.0,PI/4.] by A9,Th73,RCOMP_1:48;
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;
assume
A1: x in [.-sqrt 2,-1.];
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1}
by A1,RCOMP_1:11;then
A3: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 2;
per cases by A3,TARSKI:def 2;
suppose
A4: x in ].-sqrt 2,-1.[;
A5: -sqrt 2 in [.-sqrt 2,-1.] by A2,RCOMP_1:48;
A6: [.-sqrt 2,-1.] /\ dom arcsec2 = [.-sqrt 2,-1.] by Th46,XBOOLE_1:28;
A7: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by RCOMP_1:15;
x in {s where s is Real: -sqrt 2 < s & s < -1}
by A4,RCOMP_1:def 2;then
A8: ex s be Real st s=x & -sqrt 2 < s & s < -1;then
A9: 3/4*PI < arcsec2.x by A4,A5,A6,A7,Th74,Th82,RFUNCT_2:def 2;
-1 in [.-sqrt 2,-1.] /\ dom arcsec2 by A2,A6,RCOMP_1:48;
then arcsec2.x < PI by A4,A6,A7,A8,Th74,Th82,RFUNCT_2:def 2;
hence arcsec2.x in [.3/4*PI,PI.] by A9,RCOMP_1:48;
end;
suppose
A10: x = -sqrt 2;
3/4*PI <= PI by Lm10,RCOMP_2:4;
hence arcsec2.x in [.3/4*PI,PI.] by A10,Th74,RCOMP_1:48;
end;
suppose
A11: x = -1;
3/4*PI <= PI by Lm10,RCOMP_2:4;
hence arcsec2.x in [.3/4*PI,PI.] by A11,Th74,RCOMP_1:48;
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;
assume
A1: x in [.-sqrt 2,-1.];
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
then x in ].-sqrt 2,-1.[ \/ {-sqrt 2,-1}
by A1,RCOMP_1:11;then
A3: x in ].-sqrt 2,-1.[ or x in {-sqrt 2,-1} by XBOOLE_0:def 2;
per cases by A3,TARSKI:def 2;
suppose
A4: x in ].-sqrt 2,-1.[;
A5: -sqrt 2 in [.-sqrt 2,-1.] by A2,RCOMP_1:48;
A6: [.-sqrt 2,-1.] /\ dom arccosec1 = [.-sqrt 2,-1.] by Th47,XBOOLE_1:28;
A7: ].-sqrt 2,-1.[ c= [.-sqrt 2,-1.] by RCOMP_1:15;
x in {s where s is Real: -sqrt 2 < s & s < -1}
by A4,RCOMP_1:def 2;then
A8: ex s be Real st s=x & -sqrt 2 < s & s < -1;then
A9: -PI/4 > arccosec1.x by A4,A5,A6,A7,Th75,Th83,RFUNCT_2:def 3;
-1 in [.-sqrt 2,-1.] /\ dom arccosec1 by A2,A6,RCOMP_1:48;
then arccosec1.x > -PI/2 by A4,A6,A7,A8,Th75,Th83,RFUNCT_2:def 3;
hence arccosec1.x in [.-PI/2,-PI/4.] by A9,RCOMP_1:48;
end;
suppose
A10: x = -sqrt 2;
-PI/2 <= -PI/4 by Lm11,RCOMP_2:3;
hence arccosec1.x in [.-PI/2,-PI/4.] by A10,Th75,RCOMP_1:48;
end;
suppose
A11: x = -1;
-PI/2 <= -PI/4 by Lm11,RCOMP_2:3;
hence arccosec1.x in [.-PI/2,-PI/4.] by A11,Th75,RCOMP_1:48;
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:84,RCOMP_1:11;then
A1: x in ].1,sqrt 2.[ or x in {1,sqrt 2} by XBOOLE_0:def 2;
per cases by A1,TARSKI:def 2;
suppose
A2: x in ].1,sqrt 2.[;
A3: 1 in [.1,sqrt 2.] by SQUARE_1:84,RCOMP_1:48;
A4: [.1,sqrt 2.] /\ dom arccosec2 = [.1,sqrt 2.] by Th48,XBOOLE_1:28;
A5: ].1,sqrt 2.[ c= [.1,sqrt 2.] by RCOMP_1:15;
x in {s where s is Real: 1 < s & s < sqrt 2} by A2,RCOMP_1:def 2;then
A6: ex s be Real st s=x & 1 < s & s < sqrt 2;then
A7: PI/2 > arccosec2.x by A2,A3,A4,A5,Th76,Th84,RFUNCT_2:def 3;
sqrt 2 in [.1,sqrt 2.] /\ dom arccosec2 by A4,SQUARE_1:84,RCOMP_1:48;
then arccosec2.x > PI/4 by A2,A4,A5,A6,Th76,Th84,RFUNCT_2:def 3;
hence arccosec2.x in [.PI/4,PI/2.] by A7,RCOMP_1:48;
end;
suppose
A8: x = 1;
PI/4 <= PI/2 by Lm12,RCOMP_2:4;
hence arccosec2.x in [.PI/4,PI/2.] by A8,Th76,RCOMP_1:48;
end;
suppose
A9: x = sqrt 2;
PI/4 <= PI/2 by Lm12,RCOMP_2:4;
hence arccosec2.x in [.PI/4,PI/2.] by A9,Th76,RCOMP_1:48;
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.] by RCOMP_1:48;then
A2: r in dom (arcsec1|[.1,sqrt 2.]) by Th45,RELAT_1:91;
sec.(arcsec1 r)
= ((sec|[.0,PI/4.]) qua Function).(arcsec1.r)
by A1,Th85,FUNCT_1:72
.= ((sec|[.0,PI/4.]) qua Function).((arcsec1|[.1,sqrt 2.]).r)
by A1,FUNCT_1:72
.= ((sec|[.0,PI/4.]) qua Function * (arcsec1|[.1,sqrt 2.])).r
by A2,FUNCT_1:23
.= (id [.1,sqrt 2.]).r by Th41,Th49,FUNCT_1:61
.= r by A1,FUNCT_1:35;
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.] by RCOMP_1:48;then
A2: r in dom (arcsec2|[.-sqrt 2,-1.]) by Th46,RELAT_1:91;
sec.(arcsec2 r)
= ((sec|[.3/4*PI,PI.]) qua Function).(arcsec2.r)
by A1,Th86,FUNCT_1:72
.= ((sec|[.3/4*PI,PI.]) qua Function).((arcsec2|[.-sqrt 2,-1.]).r)
by A1,FUNCT_1:72
.= ((sec|[.3/4*PI,PI.]) qua Function * (arcsec2|[.-sqrt 2,-1.])).r
by A2,FUNCT_1:23
.= (id [.-sqrt 2,-1.]).r by Th42,Th50,FUNCT_1:61
.= r by A1,FUNCT_1:35;
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.] by RCOMP_1:48;then
A2: r in dom (arccosec1|[.-sqrt 2,-1.]) by Th47,RELAT_1:91;
cosec.(arccosec1 r)
= ((cosec|[.-PI/2,-PI/4.]) qua Function).(arccosec1.r)
by A1,Th87,FUNCT_1:72
.= ((cosec|[.-PI/2,-PI/4.]) qua Function).((arccosec1|[.-sqrt 2,-1.]).r)
by A1,FUNCT_1:72
.= ((cosec|[.-PI/2,-PI/4.]) qua Function * (arccosec1|[.-sqrt 2,-1.])).r
by A2,FUNCT_1:23
.= (id [.-sqrt 2,-1.]).r by Th43,Th51,FUNCT_1:61
.= r by A1,FUNCT_1:35;
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.] by RCOMP_1:48;then
A2: r in dom (arccosec2|[.1,sqrt 2.]) by Th48,RELAT_1:91;
cosec.(arccosec2 r)
= ((cosec|[.PI/4,PI/2.]) qua Function).(arccosec2.r)
by A1,Th88,FUNCT_1:72
.= ((cosec|[.PI/4,PI/2.]) qua Function).((arccosec2|[.1,sqrt 2.]).r)
by A1,FUNCT_1:72
.= ((cosec|[.PI/4,PI/2.]) qua Function * (arccosec2|[.1,sqrt 2.])).r
by A2,FUNCT_1:23
.= (id [.1,sqrt 2.]).r by Th44,Th52,FUNCT_1:61
.= r by A1,FUNCT_1:35;
hence thesis;
end;
theorem Th93:
arcsec1 is_continuous_on [.1,sqrt 2.]
proof
set f = sec | [.0,PI/4.];
A1: f|[.0,PI/4.] = f by RELAT_1:101;
0 <= PI/4 by Lm9,RCOMP_2:3;then
(f|[.0,PI/4.])" is_continuous_on f.:[.0,PI/4.]
by Lm13,Lm21,FCONT_1:54;
then arcsec1|[.1,sqrt 2.] is_continuous_on [.1,sqrt 2.]
by A1,Th41,Th49,RELAT_1:148;
hence arcsec1 is_continuous_on [.1,sqrt 2.] by FCONT_1:16;
end;
theorem Th94:
arcsec2 is_continuous_on [.-sqrt 2,-1.]
proof
set f = sec | [.3/4*PI,PI.];
A1: f|[.3/4*PI,PI.] = f by RELAT_1:101;
3/4*PI <= PI by Lm10,RCOMP_2:4;then
(f|[.3/4*PI,PI.])" is_continuous_on f.:[.3/4*PI,PI.]
by Lm14,Lm22,FCONT_1:54;
then arcsec2|[.-sqrt 2,-1.] is_continuous_on [.-sqrt 2,-1.]
by A1,Th42,Th50,RELAT_1:148;
hence arcsec2 is_continuous_on [.-sqrt 2,-1.] by FCONT_1:16;
end;
theorem Th95:
arccosec1 is_continuous_on [.-sqrt 2,-1.]
proof
set f = cosec | [.-PI/2,-PI/4.];
A1: f|[.-PI/2,-PI/4.] = f by RELAT_1:101;
-PI/2 <= -PI/4 by Lm11,RCOMP_2:3;then
(f|[.-PI/2,-PI/4.])" is_continuous_on f.:[.-PI/2,-PI/4.]
by Lm15,Lm23,FCONT_1:54;
then arccosec1|[.-sqrt 2,-1.] is_continuous_on [.-sqrt 2,-1.]
by A1,Th43,Th51,RELAT_1:148;
hence arccosec1 is_continuous_on [.-sqrt 2,-1.] by FCONT_1:16;
end;
theorem Th96:
arccosec2 is_continuous_on [.1,sqrt 2.]
proof
set f = cosec | [.PI/4,PI/2.];
A1: f|[.PI/4,PI/2.] = f by RELAT_1:101;
PI/4 <= PI/2 by Lm12,RCOMP_2:4;then
(f|[.PI/4,PI/2.])" is_continuous_on f.:[.PI/4,PI/2.]
by Lm16,Lm24,FCONT_1:54;
then arccosec2|[.1,sqrt 2.] is_continuous_on [.1,sqrt 2.]
by A1,Th44,Th52,RELAT_1:148;
hence arccosec2 is_continuous_on [.1,sqrt 2.] by FCONT_1:16;
end;
theorem Th97:
rng(arcsec1 | [.1,sqrt 2.]) = [.0,PI/4.]
proof
now let y be set;
thus y in [.0,PI/4.] implies
ex x be set 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 2;
then consider x be Real such that
A2: x in [.1,sqrt 2.] and
A3: y1 = arcsec1.x by Th93,SQUARE_1:84,FCONT_2:16;
take x;
thus x in dom (arcsec1 | [.1,sqrt 2.]) &
y = (arcsec1 | [.1,sqrt 2.]).x
by A2,A3,Th45,RELAT_1:91,FUNCT_1:72;
end;
thus (ex x be set st x in dom (arcsec1 | [.1,sqrt 2.]) &
y = (arcsec1 | [.1,sqrt 2.]).x) implies y in [.0,PI/4.]
proof
given x be set such that
A4: x in dom (arcsec1 | [.1,sqrt 2.]) and
A5: y = (arcsec1 | [.1,sqrt 2.]).x;
A6: dom (arcsec1 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th45,RELAT_1:91;
reconsider x1=x as Real by A4;
y = arcsec1.x by A4,A5,A6,FUNCT_1:72;
hence y in [.0,PI/4.] by A4,A6,Th85;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th98:
rng(arcsec2 | [.-sqrt 2,-1.]) = [.3/4*PI,PI.]
proof
now let y be set;
thus y in [.3/4*PI,PI.] implies
ex x be set 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;
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
y1 in [.arcsec2.(-sqrt 2),arcsec2.(-1).] \/
[.arcsec2.(-1),arcsec2.(-sqrt 2).] by A1,Th74,XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.-sqrt 2,-1.] and
A4: y1 = arcsec2.x by A2,Th94,FCONT_2:16;
take x;
thus x in dom (arcsec2 | [.-sqrt 2,-1.]) &
y = (arcsec2 | [.-sqrt 2,-1.]).x
by A3,A4,Th46,RELAT_1:91,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A5: x in dom (arcsec2 | [.-sqrt 2,-1.]) and
A6: y = (arcsec2 | [.-sqrt 2,-1.]).x;
A7: dom (arcsec2 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th46,RELAT_1:91;
reconsider x1=x as Real by A5;
y = arcsec2.x by A5,A6,A7,FUNCT_1:72;
hence y in [.3/4*PI,PI.] by A5,A7,Th86;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th99:
rng(arccosec1 | [.-sqrt 2,-1.]) = [.-PI/2,-PI/4.]
proof
now let y be set;
thus y in [.-PI/2,-PI/4.] implies
ex x be set 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;
A2: -sqrt 2 < -1 by SQUARE_1:84,XREAL_1:26;
y1 in [.arccosec1.(-1),arccosec1.(-sqrt 2).] \/
[.arccosec1.(-sqrt 2),arccosec1.(-1).] by A1,Th75,XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.-sqrt 2,-1.] and
A4: y1 = arccosec1.x by A2,Th95,FCONT_2:16;
take x;
thus x in dom (arccosec1 | [.-sqrt 2,-1.]) &
y = (arccosec1 | [.-sqrt 2,-1.]).x
by A3,A4,Th47,RELAT_1:91,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A5: x in dom (arccosec1 | [.-sqrt 2,-1.]) and
A6: y = (arccosec1 | [.-sqrt 2,-1.]).x;
A7: dom (arccosec1 | [.-sqrt 2,-1.]) = [.-sqrt 2,-1.] by Th47,RELAT_1:91;
reconsider x1=x as Real by A5;
y = arccosec1.x by A5,A6,A7,FUNCT_1:72;
hence y in [.-PI/2,-PI/4.] by A5,A7,Th87;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th100:
rng(arccosec2 | [.1,sqrt 2.]) = [.PI/4,PI/2.]
proof
now let y be set;
thus y in [.PI/4,PI/2.] implies
ex x be set 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 2;
then consider x be Real such that
A2: x in [.1,sqrt 2.] and
A3: y1 = arccosec2.x by Th96,SQUARE_1:84,FCONT_2:16;
take x;
thus x in dom (arccosec2 | [.1,sqrt 2.]) &
y = (arccosec2 | [.1,sqrt 2.]).x
by A2,A3,Th48,RELAT_1:91,FUNCT_1:72;
end;
thus (ex x be set 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 set such that
A4: x in dom (arccosec2 | [.1,sqrt 2.]) and
A5: y = (arccosec2 | [.1,sqrt 2.]).x;
A6: dom (arccosec2 | [.1,sqrt 2.]) = [.1,sqrt 2.] by Th48,RELAT_1:91;
reconsider x1=x as Real by A4;
y = arccosec2.x by A4,A5,A6,FUNCT_1:72;
hence y in [.PI/4,PI/2.] by A4,A6,Th88;
end;
end;
hence thesis by FUNCT_1:def 5;
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.] by RCOMP_1:48;
then r in dom (arcsec1 | [.1,sqrt 2.]) by Th45,RELAT_1:91;
then (arcsec1 | [.1,sqrt 2.]).r in rng(arcsec1 | [.1,sqrt 2.])
by FUNCT_1:def 5;
then arcsec1 r in rng(arcsec1 | [.1,sqrt 2.]) by A1,FUNCT_1:72;
hence thesis by Th97,RCOMP_1:48;
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.] by RCOMP_1:48;
then r in dom (arcsec2 | [.-sqrt 2,-1.]) by Th46,RELAT_1:91;
then (arcsec2 | [.-sqrt 2,-1.]).r in rng(arcsec2 | [.-sqrt 2,-1.])
by FUNCT_1:def 5;
then arcsec2 r in rng(arcsec2 | [.-sqrt 2,-1.]) by A1,FUNCT_1:72;
hence thesis by Th98,RCOMP_1:48;
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.] by RCOMP_1:48;
then r in dom (arccosec1 | [.-sqrt 2,-1.]) by Th47,RELAT_1:91;
then (arccosec1 | [.-sqrt 2,-1.]).r in rng(arccosec1 | [.-sqrt 2,-1.])
by FUNCT_1:def 5;
then arccosec1 r in rng(arccosec1 | [.-sqrt 2,-1.]) by A1,FUNCT_1:72;
hence thesis by Th99,RCOMP_1:48;
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.] by RCOMP_1:48;
then r in dom (arccosec2 | [.1,sqrt 2.]) by Th48,RELAT_1:91;
then (arccosec2 | [.1,sqrt 2.]).r in rng(arccosec2 | [.1,sqrt 2.])
by FUNCT_1:def 5;
then arccosec2 r in rng(arccosec2 | [.1,sqrt 2.]) by A1,FUNCT_1:72;
hence thesis by Th100,RCOMP_1:48;
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 0 <= arcsec1 r & arcsec1 r <= PI/4 by Th105;
then 0 < arcsec1 r & arcsec1 r < PI/4 or
0 = arcsec1 r or arcsec1 r = PI/4 by REAL_1:def 5;
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 REAL_1:def 5;
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 REAL_1:def 5;
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 REAL_1:def 5;
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
A1: 1 <= r & r <= sqrt 2;then
r in [.1,sqrt 2.] by RCOMP_1:48;then
A2: x in dom (sec | [.0,PI/4.]) by Lm13,Th85;
A3: dom (sec | [.0,PI/4.]) c= dom sec by RELAT_1:89;
A5: r = (cos^).x by A1,Th89
.= 1/cos.x by A2,A3,RFUNCT_1:def 8;
r > 0 by A1,XXREAL_0:2;then
A7: r^2 > 0 by SQUARE_1:74;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8: (sin.x)^2 = 1-(cos.x)^2
.= 1-(1/r)*(1/r) by A5
.= 1-1/(r^2) by XCMPLX_1:103
.= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
.= (r^2-1)/(r^2);
r^2 >= 1^2 by A1,SQUARE_1:77;then
A9: r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
A12: 0 in [.0,PI.] by COMPTRIG:21,RCOMP_1:48;
A13: PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;
PI/4 < PI/1 by COMPTRIG:21,REAL_2:200;
then PI/4 in [.0,PI.] by A13,RCOMP_1:48;
then [.0,PI/4.] c= [.0,PI.] by A12,RCOMP_1:16;
then sin.x >= 0 by A2,Lm13,COMPTRIG:24;
then sin.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
.= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
.= sqrt(r^2-1)/r by A1,XXREAL_0:2,SQUARE_1:89;
hence thesis by A5;
end;
theorem Th114:
-sqrt 2 <= r & r <= -1 implies sin(arcsec2 r) = -sqrt(r^2-1)/r &
cos(arcsec2 r) = 1/r
proof
set x = arcsec2 r;
assume
A1: -sqrt 2 <= r & r <= -1;then
r in [.-sqrt 2,-1.] by RCOMP_1:48;then
A2: x in dom (sec | [.3/4*PI,PI.]) by Lm14,Th86;
A3: dom (sec | [.3/4*PI,PI.]) c= dom sec by RELAT_1:89;
A5: r = (cos^).x by A1,Th90
.= 1/cos.x by A2,A3,RFUNCT_1:def 8;
r < 0 by A1,XXREAL_0:2;then
A7: r^2 > 0 by SQUARE_1:74;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8: (sin.x)^2 = 1-(cos.x)^2
.= 1-(1/r)*(1/r) by A5
.= 1-1/(r^2) by XCMPLX_1:103
.= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
.= (r^2-1)/(r^2);
-r >= -(-1) by A1,XREAL_1:26;
then (-r)^2 >= 1^2 by SQUARE_1:77;then
A9: r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
3/4*PI > PI/2 by Lm10,RCOMP_2:4;then
A11: 3/4*PI > 0 by COMPTRIG:21,XXREAL_0:2;
3/4*PI <= PI by Lm10,RCOMP_2:4;then
A12: 3/4*PI in [.0,PI.] by A11,RCOMP_1:48;
PI in [.0,PI.] by COMPTRIG:21,RCOMP_1:48;
then [.3/4*PI,PI.] c= [.0,PI.] by A12,RCOMP_1:16;
then sin.x >= 0 by A2,Lm14,COMPTRIG:24;
then sin.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
.= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
.= sqrt(r^2-1)/(-r) by A1,XXREAL_0:2,SQUARE_1:90
.= -sqrt(r^2-1)/r by XCMPLX_1:189;
hence thesis by A5;
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
A1: -sqrt 2 <= r & r <= -1;
then r in [.-sqrt 2,-1.] by RCOMP_1:48;then
A2: x in dom (cosec | [.-PI/2,-PI/4.]) by Lm15,Th87;
A3: dom (cosec | [.-PI/2,-PI/4.]) c= dom cosec by RELAT_1:89;
A8: r = (sin^).x by A1,Th91
.= 1/sin.x by A2,A3,RFUNCT_1:def 8;
r < 0 by A1,XXREAL_0:2;then
A10: r^2 > 0 by SQUARE_1:74;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A11: (cos.x)^2 = 1-(sin.x)^2
.= 1-(1/r)*(1/r) by A8
.= 1-1/(r^2) by XCMPLX_1:103
.= (r^2)/(r^2)-1/(r^2) by A10,XCMPLX_1:60
.= (r^2-1)/(r^2);
-r >= -(-1) by A1,XREAL_1:26;
then (-r)^2 >= 1^2 by SQUARE_1:77;then
A12: r^2-1 >= 0 by XREAL_1:50;then
A13: (r^2-1)/(r^2) >= 0 by A10,XREAL_1:138;
A14: -PI/2 in [.-PI/2,PI/2.] by RCOMP_1:48;
A15: -PI/4 >= -PI/2 & -PI/4 < 0 by Lm11,RCOMP_2:3;
-PI/4 in [.-PI/2,PI/2.] by A15,RCOMP_1:48;
then [.-PI/2,-PI/4.] c= [.-PI/2,PI/2.] by A14,RCOMP_1:16;
then cos.x >= 0 by A2,Lm15,COMPTRIG:28;
then cos.x = sqrt ((r^2-1)/(r^2)) by A11,A13,SQUARE_1:def 4
.= sqrt(r^2-1)/sqrt(r^2) by A10,A12,SQUARE_1:99
.= sqrt(r^2-1)/(-r) by A1,XXREAL_0:2,SQUARE_1:90
.= -sqrt(r^2-1)/r by XCMPLX_1:189;
hence thesis by A8;
end;
theorem Th116:
1 <= r & r <= sqrt 2 implies sin(arccosec2 r) = 1/r &
cos(arccosec2 r) = sqrt(r^2-1)/r
proof
set x = arccosec2 r;
assume
A1: 1 <= r & r <= sqrt 2;then
r in [.1,sqrt 2.] by RCOMP_1:48;then
A2: x in dom (cosec | [.PI/4,PI/2.]) by Lm16,Th88;
A3: dom (cosec | [.PI/4,PI/2.]) c= dom cosec by RELAT_1:89;
A5: r = (sin^).x by A1,Th92
.= 1/sin.x by A2,A3,RFUNCT_1:def 8;
r > 0 by A1,XXREAL_0:2;then
A7: r^2 > 0 by SQUARE_1:74;
(sin.x)^2+(cos.x)^2 = 1 by SIN_COS:31;then
A8: (cos.x)^2 = 1-(sin.x)^2
.= 1-(1/r)*(1/r) by A5
.= 1-1/(r^2) by XCMPLX_1:103
.= (r^2)/(r^2)-1/(r^2) by A7,XCMPLX_1:60
.= (r^2-1)/(r^2);
r^2 >= 1^2 by A1,SQUARE_1:77;then
A9: r^2-1 >= 0 by XREAL_1:50;then
A10: (r^2-1)/(r^2) >= 0 by A7,XREAL_1:138;
A11: PI/4 <= PI/2 by Lm12,RCOMP_2:4;
A12: PI/4 in [.-PI/2,PI/2.] by A11,RCOMP_1:48;
PI/2 in [.-PI/2,PI/2.] by RCOMP_1:48;
then [.PI/4,PI/2.] c= [.-PI/2,PI/2.] by A12,RCOMP_1:16;
then cos.x >= 0 by A2,Lm16,COMPTRIG:28;
then cos.x = sqrt ((r^2-1)/(r^2)) by A8,A10,SQUARE_1:def 4
.= sqrt(r^2-1)/sqrt(r^2) by A7,A9,SQUARE_1:99
.= sqrt(r^2-1)/r by A1,XXREAL_0:2,SQUARE_1:89;
hence thesis by A5;
end;
theorem
1 < r & r < sqrt 2 implies cosec(arcsec1 r) = r/sqrt(r^2-1)
proof
set x = arcsec1 r;
assume
A1: 1 < r & r < sqrt 2;
then 0 < arcsec1 r & arcsec1 r < PI/4 by Th109;then
A2: x in ].0,PI/4.[ by RCOMP_1:47;
PI/4 < PI/2 by COMPTRIG:21,REAL_2:200;then
A3: ].0,PI/4.[ c= ].0,PI/2.[ by RCOMP_1:52;
].0,PI/2.] = ].0,PI/2.[ \/ {PI/2} by COMPTRIG:21,RCOMP_2:6;
then ].0,PI/2.[ c= ].0,PI/2.] by XBOOLE_1:7;
then ].0,PI/4.[ c= ].0,PI/2.] by A3,XBOOLE_1:1;then
A4: ].0,PI/4.[ c= dom cosec by Th4,XBOOLE_1:1;
cosec.x = 1/sin.x by A2,A4,RFUNCT_1:def 8
.= 1/(sqrt(r^2-1)/r) by A1,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;
assume
A1: -sqrt 2 < r & r < -1;
then 3/4*PI < arcsec2 r & arcsec2 r < PI by Th110;then
A2: x in ].3/4*PI,PI.[ by RCOMP_1:47;
AA: ].3/4*PI,PI.[ c= dom cosec
proof
set f = sin^;
A3: ].3/4*PI,PI.[ \ sin"{0} c= dom sin \ sin"{0} by SIN_COS:27,XBOOLE_1:33;
].3/4*PI,PI.[ /\ sin"{0} = {}
proof
assume ].3/4*PI,PI.[ /\ sin"{0} <> {};
then consider rr such that
A4: rr in ].3/4*PI,PI.[ /\ sin"{0} by XBOOLE_0:def 1;
A5: rr in ].3/4*PI,PI.[ & rr in sin"{0} by A4,XBOOLE_0:def 3;then
A6: rr is Real;
3/4*PI >= 3/4*0 by COMPTRIG:21,XREAL_1:66;
then ].3/4*PI,PI.[ c= ].0,PI.[ by RCOMP_1:52;then
A7: sin.rr <> 0 by A5,A6,COMPTRIG:23;
sin.rr in {0} by A5,FUNCT_1:def 13;
hence contradiction by A7,TARSKI:def 1;
end;
then ].3/4*PI,PI.[ misses sin"{0} by XBOOLE_0:def 7;
then ].3/4*PI,PI.[ c= dom sin \ sin"{0} by A3,XBOOLE_1:83;
hence ].3/4*PI,PI.[ c= dom cosec by RFUNCT_1:def 8;
end;
cosec.x = 1/sin.x by A2,AA,RFUNCT_1:def 8
.= 1/(-sqrt(r^2-1)/r) by A1,Th114
.= -1/(sqrt(r^2-1)/r) by XCMPLX_1:189
.= -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;
assume
A1: -sqrt 2 < r & r < -1;
then -PI/2 < arccosec1 r & arccosec1 r < -PI/4 by Th111;then
A2: x in ].-PI/2,-PI/4.[ by RCOMP_1:47;
AA: ].-PI/2,-PI/4.[ c= dom sec
proof
set f = cos^;
A3: ].-PI/2,-PI/4.[ \ cos"{0} c= dom cos \ cos"{0}
by SIN_COS:27,XBOOLE_1:33;
].-PI/2,-PI/4.[ /\ cos"{0} = {}
proof
assume ].-PI/2,-PI/4.[ /\ cos"{0} <> {};
then consider rr such that
A4: rr in ].-PI/2,-PI/4.[ /\ cos"{0} by XBOOLE_0:def 1;
A5: rr in ].-PI/2,-PI/4.[ & rr in cos"{0} by A4,XBOOLE_0:def 3;then
A6: rr is Real;
].-PI/2,-PI/4.[ c= ].-PI/2,PI/2.[ by RCOMP_1:52;then
A7: cos.rr <> 0 by A5,A6,COMPTRIG:27;
cos.rr in {0} by A5,FUNCT_1:def 13;
hence contradiction by A7,TARSKI:def 1;
end;
then ].-PI/2,-PI/4.[ misses cos"{0} by XBOOLE_0:def 7;
then ].-PI/2,-PI/4.[ c= dom cos \ cos"{0} by A3,XBOOLE_1:83;
hence ].-PI/2,-PI/4.[ c= dom sec by RFUNCT_1:def 8;
end;
sec.x = 1/cos.x by A2,AA,RFUNCT_1:def 8
.= 1/(-sqrt(r^2-1)/r) by A1,Th115
.= -1/(sqrt(r^2-1)/r) by XCMPLX_1:189
.= -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;
assume
A1: 1 < r & r < sqrt 2;
then PI/4 < arccosec2 r & arccosec2 r < PI/2 by Th112;then
A2: x in ].PI/4,PI/2.[ by RCOMP_1:47;
PI/4 > 0/4 by COMPTRIG:21,XREAL_1:76;then
A3: ].PI/4,PI/2.[ c= ].0,PI/2.[ by RCOMP_1:52;
[.0,PI/2.[ = ].0,PI/2.[ \/ {0} by COMPTRIG:21,RCOMP_2:5;
then ].0,PI/2.[ c= [.0,PI/2.[ by XBOOLE_1:7;
then ].PI/4,PI/2.[ c= [.0,PI/2.[ by A3,XBOOLE_1:1;then
A4: ].PI/4,PI/2.[ c= dom sec by Th1,XBOOLE_1:1;
sec.x = 1/cos.x by A2,A4,RFUNCT_1:def 8
.= 1/(sqrt(r^2-1)/r) by A1,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 f = sec|[.0,PI/2.[;
set g = f|].0,PI/2.[;
set g1 = arcsec1|(sec.:].0,PI/2.[);
set X = sec.:].0,PI/2.[;
A0: ].0,PI/2.[ c= [.0,PI/2.[ by RCOMP_2:17;then
A1: g = sec|].0,PI/2.[ by RELAT_1:103;
A2: dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:55
.= rng(sec|].0,PI/2.[) by A1,RELAT_1:101
.= sec.:].0,PI/2.[ by RELAT_1:148;
A3: g is_differentiable_on ].0,PI/2.[ by A1,Th5,FDIFF_2:16;
AA: now
let x0 be Real such that
A4: x0 in ].0,PI/2.[;
A5: diff(g,x0) = (g`|].0,PI/2.[).x0 by A3,A4,FDIFF_1:def 8
.= ((sec|].0,PI/2.[)`|].0,PI/2.[).x0 by A0,RELAT_1:103
.= (sec`|].0,PI/2.[).x0 by Th5,FDIFF_2:16
.= diff(sec,x0) by A4,Th5,FDIFF_1:def 8
.= sin.x0/(cos.x0)^2 by A4,Th5;
for x0 be Real st x0 in ].0,PI/2.[ holds sin.x0/(cos.x0)^2 > 0
proof
let x0 be Real;
assume
A6: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;then
A7: sin.x0 > 0 by A6,COMPTRIG:23;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A6,COMPTRIG:27;
then (cos.x0)^2 > 0 by SQUARE_1:74;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A7,REAL_1:73;
hence sin.x0/(cos.x0)^2 > 0;
end;
hence diff(g,x0) > 0 by A4,A5;
end;
AB: (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:101
.= arcsec1|(f.:].0,PI/2.[) by RFUNCT_2:40
.= arcsec1|(rng(f|].0,PI/2.[)) by RELAT_1:148
.= arcsec1|(rng (sec|].0,PI/2.[)) by A0,RELAT_1:103
.= arcsec1|(sec.:].0,PI/2.[) by RELAT_1:148;then
A9: g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arcsec1 by A2,AB,RELAT_1:89;
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 7;
hence arcsec1|X is_differentiable_in x by RELAT_1:101;
end;
hence arcsec1 is_differentiable_on sec.:].0,PI/2.[ by A11,FDIFF_1:def 7;
end;
theorem Th122:
arcsec2 is_differentiable_on sec.:].PI/2,PI.[
proof
set f = sec|].PI/2,PI.];
set g = f|].PI/2,PI.[;
set g1 = arcsec2|(sec.:].PI/2,PI.[);
set X = sec.:].PI/2,PI.[;
A0: ].PI/2,PI.[ c= ].PI/2,PI.] by RCOMP_2:17;then
A1: g = sec|].PI/2,PI.[ by RELAT_1:103;
A2: dom ((g|].PI/2,PI.[)") = rng (g|].PI/2,PI.[) by FUNCT_1:55
.= rng(sec|].PI/2,PI.[) by A1,RELAT_1:101
.= sec.:].PI/2,PI.[ by RELAT_1:148;
A3: g is_differentiable_on ].PI/2,PI.[ by A1,Th6,FDIFF_2:16;
AA: now
let x0 be Real such that
A4: x0 in ].PI/2,PI.[;
A5: diff(g,x0) = (g`|].PI/2,PI.[).x0 by A3,A4,FDIFF_1:def 8
.= ((sec|].PI/2,PI.[)`|].PI/2,PI.[).x0 by A0,RELAT_1:103
.= (sec`|].PI/2,PI.[).x0 by Th6,FDIFF_2:16
.= diff(sec,x0) by A4,Th6,FDIFF_1:def 8
.= sin.x0/(cos.x0)^2 by A4,Th6;
for x0 be Real st x0 in ].PI/2,PI.[ holds sin.x0/(cos.x0)^2 > 0
proof
let x0 be Real;
assume
A6: x0 in ].PI/2,PI.[;
].PI/2,PI.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;then
A7: sin.x0 > 0 by A6,COMPTRIG:23;
].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 < 0 by A6,COMPTRIG:29;
then (cos.x0)^2 > 0 by SQUARE_1:74;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A7,REAL_1:73;
hence sin.x0/(cos.x0)^2 > 0;
end;
hence diff(g,x0) > 0 by A4,A5;
end;
AB: (g|].PI/2,PI.[)" = (f|].PI/2,PI.[)" by RELAT_1:101
.= arcsec2|(f.:].PI/2,PI.[) by RFUNCT_2:40
.= arcsec2|(rng(f|].PI/2,PI.[)) by RELAT_1:148
.= arcsec2|(rng (sec|].PI/2,PI.[)) by A0,RELAT_1:103
.= arcsec2|(sec.:].PI/2,PI.[) by RELAT_1:148;then
A9: g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arcsec2 by A2,AB,RELAT_1:89;
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 7;
hence arcsec2|X is_differentiable_in x by RELAT_1:101;
end;
hence arcsec2 is_differentiable_on sec.:].PI/2,PI.[
by A11,FDIFF_1:def 7;
end;
theorem Th123:
arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
proof
set f = cosec|[.-PI/2,0.[;
set g = f|].-PI/2,0.[;
set g1 = arccosec1|(cosec.:].-PI/2,0.[);
set X = cosec.:].-PI/2,0.[;
A0: ].-PI/2,0.[ c= [.-PI/2,0.[ by RCOMP_2:17;then
A1: g = cosec|].-PI/2,0.[ by RELAT_1:103;
A2: dom ((g|].-PI/2,0.[)") = rng (g|].-PI/2,0.[) by FUNCT_1:55
.= rng(cosec|].-PI/2,0.[) by A1,RELAT_1:101
.= cosec.:].-PI/2,0.[ by RELAT_1:148;
A3: g is_differentiable_on ].-PI/2,0.[ by A1,Th7,FDIFF_2:16;
AA: now
let x0 be Real such that
A4: x0 in ].-PI/2,0.[;
A5: diff(g,x0) = (g`|].-PI/2,0.[).x0 by A3,A4,FDIFF_1:def 8
.= ((cosec|].-PI/2,0.[)`|].-PI/2,0.[).x0
by A0,RELAT_1:103
.= (cosec`|].-PI/2,0.[).x0 by Th7,FDIFF_2:16
.= diff(cosec,x0) by A4,Th7,FDIFF_1:def 8
.= -cos.x0/(sin.x0)^2 by A4,Th7;
for x0 be Real st x0 in ].-PI/2,0.[ holds -cos.x0/(sin.x0)^2 < 0
proof
let x0 be Real;
assume
A6: x0 in ].-PI/2,0.[;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,RCOMP_2:5;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3,XBOOLE_1:1;
then -PI < x0 & x0 < 0 by A6,RCOMP_1:47;
then -PI+2*PI < x0+2*PI & x0+2*PI < 0+2*PI by XREAL_1:10;
then x0+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(x0+2*PI) < 0 by COMPTRIG:25;
then sin.x0 < 0 by SIN_COS:83;then
A7: (sin.x0)^2 > 0 by SQUARE_1:74;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A6,COMPTRIG:27;
then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A7,REAL_1:73;
then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
hence -cos.x0/(sin.x0)^2 < 0;
end;
hence diff(g,x0) < 0 by A4,A5;
end;
AB: (g|].-PI/2,0.[)" = (f|].-PI/2,0.[)" by RELAT_1:101
.= arccosec1|(f.:].-PI/2,0.[) by RFUNCT_2:40
.= arccosec1|(rng(f|].-PI/2,0.[)) by RELAT_1:148
.= arccosec1|(rng (cosec|].-PI/2,0.[)) by A0,RELAT_1:103
.= arccosec1|(cosec.:].-PI/2,0.[) by RELAT_1:148;then
A9: g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arccosec1 by A2,AB,RELAT_1:89;
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 A9,FDIFF_1:def 7;
hence arccosec1|X is_differentiable_in x by RELAT_1:101;
end;
hence arccosec1 is_differentiable_on cosec.:].-PI/2,0.[
by A11,FDIFF_1:def 7;
end;
theorem Th124:
arccosec2 is_differentiable_on cosec.:].0,PI/2.[
proof
set f = cosec|].0,PI/2.];
set g = f|].0,PI/2.[;
set g1 = arccosec2|(cosec.:].0,PI/2.[);
set X = cosec.:].0,PI/2.[;
A0: ].0,PI/2.[ c= ].0,PI/2.] by RCOMP_2:17;then
A1: g = cosec|].0,PI/2.[ by RELAT_1:103;
A2: dom ((g|].0,PI/2.[)") = rng (g|].0,PI/2.[) by FUNCT_1:55
.= rng(cosec|].0,PI/2.[) by A1,RELAT_1:101
.= cosec.:].0,PI/2.[ by RELAT_1:148;
A3: g is_differentiable_on ].0,PI/2.[ by A1,Th8,FDIFF_2:16;
AA: now
let x0 be Real such that
A4: x0 in ].0,PI/2.[;
A5: diff(g,x0) = (g`|].0,PI/2.[).x0 by A3,A4,FDIFF_1:def 8
.= ((cosec|].0,PI/2.[)`|].0,PI/2.[).x0 by A0,RELAT_1:103
.= (cosec`|].0,PI/2.[).x0 by Th8,FDIFF_2:16
.= diff(cosec,x0) by A4,Th8,FDIFF_1:def 8
.= -cos.x0/(sin.x0)^2 by A4,Th8;
for x0 be Real st x0 in ].0,PI/2.[ holds -cos.x0/(sin.x0)^2 < 0
proof
let x0 be Real;
assume
A6: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;
then sin.x0 > 0 by A6,COMPTRIG:23;then
A7: (sin.x0)^2 > 0 by SQUARE_1:74;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A6,COMPTRIG:27;
then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A7,REAL_1:73;
then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
hence -cos.x0/(sin.x0)^2 < 0;
end;
hence diff(g,x0) < 0 by A4,A5;
end;
AB: (g|].0,PI/2.[)" = (f|].0,PI/2.[)" by RELAT_1:101
.= arccosec2|(f.:].0,PI/2.[) by RFUNCT_2:40
.= arccosec2|(rng(f|].0,PI/2.[)) by RELAT_1:148
.= arccosec2|(rng (cosec|].0,PI/2.[)) by A0,RELAT_1:103
.= arccosec2|(cosec.:].0,PI/2.[) by RELAT_1:148;then
A9: g1 is_differentiable_on X by A2,A3,AA,FDIFF_2:48;
A11: X c= dom arccosec2 by A2,AB,RELAT_1:89;
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 7;
hence arccosec2|X is_differentiable_in x by RELAT_1:101;
end;
hence arccosec2 is_differentiable_on cosec.:].0,PI/2.[
by A11,FDIFF_1:def 7;
end;
theorem
sec.:].0,PI/2.[ is open
proof
for x0 be Real st x0 in ].0,PI/2.[ holds diff(sec,x0) > 0
proof
let x0 be Real;
assume
A1: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;then
A2: sin.x0 > 0 by A1,COMPTRIG:23;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A1,COMPTRIG:27;
then (cos.x0)^2 > 0 by SQUARE_1:74;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2,REAL_1:73;
hence diff(sec,x0) > 0 by A1,Th5;
end;
then rng(sec|].0,PI/2.[) is open by Th5,FDIFF_2:41;
hence sec.:].0,PI/2.[ is open by RELAT_1:148;
end;
theorem
sec.:].PI/2,PI.[ is open
proof
for x0 be Real st x0 in ].PI/2,PI.[ holds diff(sec,x0) > 0
proof
let x0 be Real;
assume
A1: x0 in ].PI/2,PI.[;
].PI/2,PI.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;then
A2: sin.x0 > 0 by A1,COMPTRIG:23;
].PI/2,PI.[ c= ].PI/2,3/2*PI.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 < 0 by A1,COMPTRIG:29;
then (cos.x0)^2 > 0 by SQUARE_1:74;
then sin.x0/(cos.x0)^2 > 0/(cos.x0)^2 by A2,REAL_1:73;
hence diff(sec,x0) > 0 by A1,Th6;
end;
then rng(sec|].PI/2,PI.[) is open by Th6,FDIFF_2:41;
hence sec.:].PI/2,PI.[ is open by RELAT_1:148;
end;
theorem
cosec.:].-PI/2,0.[ is open
proof
for x0 be Real st x0 in ].-PI/2,0.[ holds diff(cosec,x0) < 0
proof
let x0 be Real;
assume
A1: x0 in ].-PI/2,0.[;
].-PI/2,0.[ \/ {-PI/2} = [.-PI/2,0.[ by COMPTRIG:21,RCOMP_2:5;
then ].-PI/2,0.[ c= [.-PI/2,0.[ by XBOOLE_1:7;
then ].-PI/2,0.[ c= ].-PI,0.[ by Lm3,XBOOLE_1:1;
then -PI < x0 & x0 < 0 by A1,RCOMP_1:47;
then -PI+2*PI < x0+2*PI & x0+2*PI < 0+2*PI by XREAL_1:10;
then x0+2*PI in ].PI,2*PI.[ by RCOMP_1:47;
then sin.(x0+2*PI) < 0 by COMPTRIG:25;
then sin.x0 < 0 by SIN_COS:83;then
A2: (sin.x0)^2 > 0 by SQUARE_1:74;
].-PI/2,0.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A1,COMPTRIG:27;
then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A2,REAL_1:73;
then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
hence diff(cosec,x0) < 0 by A1,Th7;
end;
then rng(cosec|].-PI/2,0.[) is open by Th7,FDIFF_2:41;
hence cosec.:].-PI/2,0.[ is open by RELAT_1:148;
end;
theorem
cosec.:].0,PI/2.[ is open
proof
for x0 be Real st x0 in ].0,PI/2.[ holds diff(cosec,x0) < 0
proof
let x0 be Real;
assume
A1: x0 in ].0,PI/2.[;
].0,PI/2.[ c= ].0,PI.[ by COMPTRIG:21,RCOMP_1:52;
then sin.x0 > 0 by A1,COMPTRIG:23;then
A2: (sin.x0)^2 > 0 by SQUARE_1:74;
].0,PI/2.[ c= ].-PI/2,PI/2.[ by COMPTRIG:21,RCOMP_1:52;
then cos.x0 > 0 by A1,COMPTRIG:27;
then cos.x0/(sin.x0)^2 > 0/(sin.x0)^2 by A2,REAL_1:73;
then -(cos.x0/(sin.x0)^2) < -0 by XREAL_1:26;
hence diff(cosec,x0) < 0 by A1,Th8;
end;
then rng(cosec|].0,PI/2.[) is open by Th8,FDIFF_2:41;
hence cosec.:].0,PI/2.[ is open by RELAT_1:148;
end;
theorem
arcsec1 is_continuous_on sec.:].0,PI/2.[ by Th121,FDIFF_1:33;
theorem
arcsec2 is_continuous_on sec.:].PI/2,PI.[ by Th122,FDIFF_1:33;
theorem
arccosec1 is_continuous_on cosec.:].-PI/2,0.[ by Th123,FDIFF_1:33;
theorem
arccosec2 is_continuous_on cosec.:].0,PI/2.[ by Th124,FDIFF_1:33;