:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

Lm1: [.0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
proof end;

theorem Th1: :: SINCOS10:1
[.0,(PI / 2).[ c= dom sec
proof end;

Lm2: ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[
proof end;

theorem Th2: :: SINCOS10:2
].(PI / 2),PI.] c= dom sec
proof end;

Lm3: [.(- (PI / 2)),0.[ c= ].(- PI),0.[
proof end;

theorem Th3: :: SINCOS10:3
[.(- (PI / 2)),0.[ c= dom cosec
proof end;

Lm4: ].0,(PI / 2).] c= ].0,PI.[
proof end;

theorem Th4: :: SINCOS10:4
].0,(PI / 2).] c= dom cosec
proof end;

theorem Th5: :: SINCOS10:5
( sec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds
diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
proof end;

theorem Th6: :: SINCOS10:6
( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds
diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
proof end;

theorem Th7: :: SINCOS10:7
( cosec is_differentiable_on ].(- (PI / 2)),0.[ & ( for x being Real st x in ].(- (PI / 2)),0.[ holds
diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
proof end;

theorem Th8: :: SINCOS10:8
( cosec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds
diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
proof end;

theorem :: SINCOS10:9
sec | ].0,(PI / 2).[ is continuous by Th5, FDIFF_1:25;

theorem :: SINCOS10:10
sec | ].(PI / 2),PI.[ is continuous by Th6, FDIFF_1:25;

theorem :: SINCOS10:11
cosec | ].(- (PI / 2)),0.[ is continuous by Th7, FDIFF_1:25;

theorem :: SINCOS10:12
cosec | ].0,(PI / 2).[ is continuous by Th8, FDIFF_1:25;

Lm5: ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ )
proof end;

Lm6: ( (3 / 4) * PI in ].(PI / 2),PI.] & PI in ].(PI / 2),PI.] )
proof end;

Lm7: ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ )
proof end;

Lm8: ( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] )
proof end;

Lm9: ].0,(PI / 2).[ c= [.0,(PI / 2).[
by XXREAL_1:22;

then Lm10: ].0,(PI / 2).[ c= dom sec
by Th1, XBOOLE_1:1;

Lm11: ].(PI / 2),PI.[ c= ].(PI / 2),PI.]
by XXREAL_1:21;

then Lm12: ].(PI / 2),PI.[ c= dom sec
by Th2, XBOOLE_1:1;

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, XBOOLE_1:1;

Lm17: ].0,(PI / 2).[ c= ].0,(PI / 2).]
by XXREAL_1:21;

then Lm18: ].0,(PI / 2).[ c= dom cosec
by Th4, XBOOLE_1:1;

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: :: SINCOS10:13
sec | ].0,(PI / 2).[ is increasing
proof end;

theorem Th14: :: SINCOS10:14
sec | ].(PI / 2),PI.[ is increasing
proof end;

theorem Th15: :: SINCOS10:15
cosec | ].(- (PI / 2)),0.[ is decreasing
proof end;

theorem Th16: :: SINCOS10:16
cosec | ].0,(PI / 2).[ is decreasing
proof end;

theorem Th17: :: SINCOS10:17
sec | [.0,(PI / 2).[ is increasing
proof end;

theorem Th18: :: SINCOS10:18
sec | ].(PI / 2),PI.] is increasing
proof end;

theorem Th19: :: SINCOS10:19
cosec | [.(- (PI / 2)),0.[ is decreasing
proof end;

theorem Th20: :: SINCOS10:20
cosec | ].0,(PI / 2).] is decreasing
proof end;

theorem :: SINCOS10:21
sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8;

theorem :: SINCOS10:22
sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8;

theorem :: SINCOS10:23
cosec | [.(- (PI / 2)),0.[ is one-to-one by Th19, FCONT_3:8;

theorem :: SINCOS10:24
cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8;

registration
cluster K77(sec,[.0,(PI / 2).[) -> one-to-one ;
coherence
sec | [.0,(PI / 2).[ is one-to-one
by Th17, FCONT_3:8;
cluster K77(sec,].(PI / 2),PI.]) -> one-to-one ;
coherence
sec | ].(PI / 2),PI.] is one-to-one
by Th18, FCONT_3:8;
cluster K77(cosec,[.(- (PI / 2)),0.[) -> one-to-one ;
coherence
cosec | [.(- (PI / 2)),0.[ is one-to-one
by Th19, FCONT_3:8;
cluster K77(cosec,].0,(PI / 2).]) -> one-to-one ;
coherence
cosec | ].0,(PI / 2).] is one-to-one
by Th20, FCONT_3:8;
end;

definition
func arcsec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 1
(sec | [.0,(PI / 2).[) " ;
coherence
(sec | [.0,(PI / 2).[) " is PartFunc of REAL,REAL
;
func arcsec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 2
(sec | ].(PI / 2),PI.]) " ;
coherence
(sec | ].(PI / 2),PI.]) " is PartFunc of REAL,REAL
;
func arccosec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 3
(cosec | [.(- (PI / 2)),0.[) " ;
coherence
(cosec | [.(- (PI / 2)),0.[) " is PartFunc of REAL,REAL
;
func arccosec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 4
(cosec | ].0,(PI / 2).]) " ;
coherence
(cosec | ].0,(PI / 2).]) " is PartFunc of REAL,REAL
;
end;

:: deftheorem defines arcsec1 SINCOS10:def 1 :
arcsec1 = (sec | [.0,(PI / 2).[) " ;

:: deftheorem defines arcsec2 SINCOS10:def 2 :
arcsec2 = (sec | ].(PI / 2),PI.]) " ;

:: deftheorem defines arccosec1 SINCOS10:def 3 :
arccosec1 = (cosec | [.(- (PI / 2)),0.[) " ;

:: deftheorem defines arccosec2 SINCOS10:def 4 :
arccosec2 = (cosec | ].0,(PI / 2).]) " ;

definition
let r be Real;
func arcsec1 r -> set equals :: SINCOS10:def 5
arcsec1 . r;
coherence
arcsec1 . r is set
;
func arcsec2 r -> set equals :: SINCOS10:def 6
arcsec2 . r;
coherence
arcsec2 . r is set
;
func arccosec1 r -> set equals :: SINCOS10:def 7
arccosec1 . r;
coherence
arccosec1 . r is set
;
func arccosec2 r -> set equals :: SINCOS10:def 8
arccosec2 . r;
coherence
arccosec2 . r is set
;
end;

:: deftheorem defines arcsec1 SINCOS10:def 5 :
for r being Real holds arcsec1 r = arcsec1 . r;

:: deftheorem defines arcsec2 SINCOS10:def 6 :
for r being Real holds arcsec2 r = arcsec2 . r;

:: deftheorem defines arccosec1 SINCOS10:def 7 :
for r being Real holds arccosec1 r = arccosec1 . r;

:: deftheorem defines arccosec2 SINCOS10:def 8 :
for r being Real holds arccosec2 r = arccosec2 . r;

definition
let r be Real;
:: original: arcsec1
redefine func arcsec1 r -> Real;
coherence
arcsec1 r is Real
;
:: original: arcsec2
redefine func arcsec2 r -> Real;
coherence
arcsec2 r is Real
;
:: original: arccosec1
redefine func arccosec1 r -> Real;
coherence
arccosec1 r is Real
;
:: original: arccosec2
redefine func arccosec2 r -> Real;
coherence
arccosec2 r is Real
;
end;

Lm25: arcsec1 " = sec | [.0,(PI / 2).[
by FUNCT_1:43;

Lm26: arcsec2 " = sec | ].(PI / 2),PI.]
by FUNCT_1:43;

Lm27: arccosec1 " = cosec | [.(- (PI / 2)),0.[
by FUNCT_1:43;

Lm28: arccosec2 " = cosec | ].0,(PI / 2).]
by FUNCT_1:43;

theorem Th25: :: SINCOS10:25
rng arcsec1 = [.0,(PI / 2).[
proof end;

theorem Th26: :: SINCOS10:26
rng arcsec2 = ].(PI / 2),PI.]
proof end;

theorem Th27: :: SINCOS10:27
rng arccosec1 = [.(- (PI / 2)),0.[
proof end;

theorem Th28: :: SINCOS10:28
rng arccosec2 = ].0,(PI / 2).]
proof end;

registration
cluster arcsec1 -> one-to-one ;
coherence
arcsec1 is one-to-one
;
cluster arcsec2 -> one-to-one ;
coherence
arcsec2 is one-to-one
;
cluster arccosec1 -> one-to-one ;
coherence
arccosec1 is one-to-one
;
cluster arccosec2 -> one-to-one ;
coherence
arccosec2 is one-to-one
;
end;

theorem Th29: :: SINCOS10:29
( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) )
proof end;

theorem Th30: :: SINCOS10:30
( 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 end;

theorem Th31: :: SINCOS10:31
( sec . 0 = 1 & sec . (PI / 4) = sqrt 2 & sec . ((3 / 4) * PI) = - (sqrt 2) & sec . PI = - 1 )
proof end;

theorem Th32: :: SINCOS10:32
( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 )
proof end;

theorem Th33: :: SINCOS10:33
for x being set st x in [.0,(PI / 4).] holds
sec . x in [.1,(sqrt 2).]
proof end;

theorem Th34: :: SINCOS10:34
for x being set st x in [.((3 / 4) * PI),PI.] holds
sec . x in [.(- (sqrt 2)),(- 1).]
proof end;

theorem Th35: :: SINCOS10:35
for x being set st x in [.(- (PI / 2)),(- (PI / 4)).] holds
cosec . x in [.(- (sqrt 2)),(- 1).]
proof end;

theorem Th36: :: SINCOS10:36
for x being set st x in [.(PI / 4),(PI / 2).] holds
cosec . x in [.1,(sqrt 2).]
proof end;

Lm29: dom (sec | [.0,(PI / 4).]) = [.0,(PI / 4).]
proof end;

Lm30: dom (sec | [.((3 / 4) * PI),PI.]) = [.((3 / 4) * PI),PI.]
proof end;

Lm31: dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).]
proof end;

Lm32: dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).]
proof end;

Lm33: ( dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ & ( for th being real number st th in [.0,(PI / 2).[ holds
(sec | [.0,(PI / 2).[) . th = sec . th ) )

proof end;

Lm34: ( dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] & ( for th being real number st th in ].(PI / 2),PI.] holds
(sec | ].(PI / 2),PI.]) . th = sec . th ) )

proof end;

Lm35: ( dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ & ( for th being real number st th in [.(- (PI / 2)),0.[ holds
(cosec | [.(- (PI / 2)),0.[) . th = cosec . th ) )

proof end;

Lm36: ( dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] & ( for th being real number st th in ].0,(PI / 2).] holds
(cosec | ].0,(PI / 2).]) . th = cosec . th ) )

proof end;

theorem Th37: :: SINCOS10:37
sec | [.0,(PI / 2).[ is continuous
proof end;

theorem Th38: :: SINCOS10:38
sec | ].(PI / 2),PI.] is continuous
proof end;

theorem Th39: :: SINCOS10:39
cosec | [.(- (PI / 2)),0.[ is continuous
proof end;

theorem Th40: :: SINCOS10:40
cosec | ].0,(PI / 2).] is continuous
proof end;

theorem Th41: :: SINCOS10:41
rng (sec | [.0,(PI / 4).]) = [.1,(sqrt 2).]
proof end;

theorem Th42: :: SINCOS10:42
rng (sec | [.((3 / 4) * PI),PI.]) = [.(- (sqrt 2)),(- 1).]
proof end;

theorem Th43: :: SINCOS10:43
rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (sqrt 2)),(- 1).]
proof end;

theorem Th44: :: SINCOS10:44
rng (cosec | [.(PI / 4),(PI / 2).]) = [.1,(sqrt 2).]
proof end;

theorem Th45: :: SINCOS10:45
[.1,(sqrt 2).] c= dom arcsec1
proof end;

theorem Th46: :: SINCOS10:46
[.(- (sqrt 2)),(- 1).] c= dom arcsec2
proof end;

theorem Th47: :: SINCOS10:47
[.(- (sqrt 2)),(- 1).] c= dom arccosec1
proof end;

theorem Th48: :: SINCOS10:48
[.1,(sqrt 2).] c= dom arccosec2
proof end;

Lm37: (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] is increasing
proof end;

Lm38: (sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] is increasing
proof end;

Lm39: (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is decreasing
proof end;

Lm40: (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing
proof end;

Lm41: sec | [.0,(PI / 4).] is one-to-one
proof end;

Lm42: sec | [.((3 / 4) * PI),PI.] is one-to-one
proof end;

Lm43: cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one
proof end;

Lm44: cosec | [.(PI / 4),(PI / 2).] is one-to-one
proof end;

registration
cluster K77(sec,[.0,(PI / 4).]) -> one-to-one ;
coherence
sec | [.0,(PI / 4).] is one-to-one
by Lm41;
cluster K77(sec,[.((3 / 4) * PI),PI.]) -> one-to-one ;
coherence
sec | [.((3 / 4) * PI),PI.] is one-to-one
by Lm42;
cluster K77(cosec,[.(- (PI / 2)),(- (PI / 4)).]) -> one-to-one ;
coherence
cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one
by Lm43;
cluster K77(cosec,[.(PI / 4),(PI / 2).]) -> one-to-one ;
coherence
cosec | [.(PI / 4),(PI / 2).] is one-to-one
by Lm44;
end;

theorem Th49: :: SINCOS10:49
arcsec1 | [.1,(sqrt 2).] = (sec | [.0,(PI / 4).]) "
proof end;

theorem Th50: :: SINCOS10:50
arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI),PI.]) "
proof end;

theorem Th51: :: SINCOS10:51
arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) "
proof end;

theorem Th52: :: SINCOS10:52
arccosec2 | [.1,(sqrt 2).] = (cosec | [.(PI / 4),(PI / 2).]) "
proof end;

theorem :: SINCOS10:53
(sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39;

theorem :: SINCOS10:54
(sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39;

theorem :: SINCOS10:55
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39;

theorem :: SINCOS10:56
(cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39;

theorem :: SINCOS10:57
(sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39;

theorem :: SINCOS10:58
(sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39;

theorem :: SINCOS10:59
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39;

theorem :: SINCOS10:60
(cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39;

theorem :: SINCOS10:61
arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39;

theorem :: SINCOS10:62
arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39;

theorem :: SINCOS10:63
arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39;

theorem :: SINCOS10:64
arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39;

theorem Th65: :: SINCOS10:65
arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39;

theorem Th66: :: SINCOS10:66
arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39;

theorem Th67: :: SINCOS10:67
arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39;

theorem Th68: :: SINCOS10:68
arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39;

theorem Th69: :: SINCOS10:69
for r being Real st 0 <= r & r < PI / 2 holds
arcsec1 (sec . r) = r
proof end;

theorem Th70: :: SINCOS10:70
for r being Real st PI / 2 < r & r <= PI holds
arcsec2 (sec . r) = r
proof end;

theorem Th71: :: SINCOS10:71
for r being Real st - (PI / 2) <= r & r < 0 holds
arccosec1 (cosec . r) = r
proof end;

theorem Th72: :: SINCOS10:72
for r being Real st 0 < r & r <= PI / 2 holds
arccosec2 (cosec . r) = r
proof end;

theorem Th73: :: SINCOS10:73
( arcsec1 . 1 = 0 & arcsec1 . (sqrt 2) = PI / 4 )
proof end;

theorem Th74: :: SINCOS10:74
( arcsec2 . (- (sqrt 2)) = (3 / 4) * PI & arcsec2 . (- 1) = PI )
proof end;

theorem Th75: :: SINCOS10:75
( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) )
proof end;

theorem Th76: :: SINCOS10:76
( arccosec2 . (sqrt 2) = PI / 4 & arccosec2 . 1 = PI / 2 )
proof end;

theorem Th77: :: SINCOS10:77
arcsec1 | (sec .: [.0,(PI / 2).[) is increasing
proof end;

theorem Th78: :: SINCOS10:78
arcsec2 | (sec .: ].(PI / 2),PI.]) is increasing
proof end;

theorem Th79: :: SINCOS10:79
arccosec1 | (cosec .: [.(- (PI / 2)),0.[) is decreasing
proof end;

theorem Th80: :: SINCOS10:80
arccosec2 | (cosec .: ].0,(PI / 2).]) is decreasing
proof end;

theorem Th81: :: SINCOS10:81
arcsec1 | [.1,(sqrt 2).] is increasing
proof end;

theorem Th82: :: SINCOS10:82
arcsec2 | [.(- (sqrt 2)),(- 1).] is increasing
proof end;

theorem Th83: :: SINCOS10:83
arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing
proof end;

theorem Th84: :: SINCOS10:84
arccosec2 | [.1,(sqrt 2).] is decreasing
proof end;

theorem Th85: :: SINCOS10:85
for x being set st x in [.1,(sqrt 2).] holds
arcsec1 . x in [.0,(PI / 4).]
proof end;

theorem Th86: :: SINCOS10:86
for x being set st x in [.(- (sqrt 2)),(- 1).] holds
arcsec2 . x in [.((3 / 4) * PI),PI.]
proof end;

theorem Th87: :: SINCOS10:87
for x being set st x in [.(- (sqrt 2)),(- 1).] holds
arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).]
proof end;

theorem Th88: :: SINCOS10:88
for x being set st x in [.1,(sqrt 2).] holds
arccosec2 . x in [.(PI / 4),(PI / 2).]
proof end;

theorem Th89: :: SINCOS10:89
for r being Real st 1 <= r & r <= sqrt 2 holds
sec . (arcsec1 r) = r
proof end;

theorem Th90: :: SINCOS10:90
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
sec . (arcsec2 r) = r
proof end;

theorem Th91: :: SINCOS10:91
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
cosec . (arccosec1 r) = r
proof end;

theorem Th92: :: SINCOS10:92
for r being Real st 1 <= r & r <= sqrt 2 holds
cosec . (arccosec2 r) = r
proof end;

theorem Th93: :: SINCOS10:93
arcsec1 | [.1,(sqrt 2).] is continuous
proof end;

theorem Th94: :: SINCOS10:94
arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous
proof end;

theorem Th95: :: SINCOS10:95
arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous
proof end;

theorem Th96: :: SINCOS10:96
arccosec2 | [.1,(sqrt 2).] is continuous
proof end;

theorem Th97: :: SINCOS10:97
rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).]
proof end;

theorem Th98: :: SINCOS10:98
rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.((3 / 4) * PI),PI.]
proof end;

theorem Th99: :: SINCOS10:99
rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (PI / 2)),(- (PI / 4)).]
proof end;

theorem Th100: :: SINCOS10:100
rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).]
proof end;

theorem :: SINCOS10:101
for r being Real holds
( ( 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 :: SINCOS10:102
for r being Real holds
( ( - (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 :: SINCOS10:103
for r being Real holds
( ( - (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 :: SINCOS10:104
for r being Real holds
( ( 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: :: SINCOS10:105
for r being Real st 1 <= r & r <= sqrt 2 holds
( 0 <= arcsec1 r & arcsec1 r <= PI / 4 )
proof end;

theorem Th106: :: SINCOS10:106
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI )
proof end;

theorem Th107: :: SINCOS10:107
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) )
proof end;

theorem Th108: :: SINCOS10:108
for r being Real st 1 <= r & r <= sqrt 2 holds
( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 )
proof end;

theorem Th109: :: SINCOS10:109
for r being Real st 1 < r & r < sqrt 2 holds
( 0 < arcsec1 r & arcsec1 r < PI / 4 )
proof end;

theorem Th110: :: SINCOS10:110
for r being Real st - (sqrt 2) < r & r < - 1 holds
( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI )
proof end;

theorem Th111: :: SINCOS10:111
for r being Real st - (sqrt 2) < r & r < - 1 holds
( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) )
proof end;

theorem Th112: :: SINCOS10:112
for r being Real st 1 < r & r < sqrt 2 holds
( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 )
proof end;

theorem Th113: :: SINCOS10:113
for r being Real st 1 <= r & r <= sqrt 2 holds
( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r )
proof end;

theorem Th114: :: SINCOS10:114
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r )
proof end;

theorem Th115: :: SINCOS10:115
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) )
proof end;

theorem Th116: :: SINCOS10:116
for r being Real st 1 <= r & r <= sqrt 2 holds
( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r )
proof end;

theorem :: SINCOS10:117
for r being Real st 1 < r & r < sqrt 2 holds
cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1))
proof end;

theorem :: SINCOS10:118
for r being Real st - (sqrt 2) < r & r < - 1 holds
cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1)))
proof end;

theorem :: SINCOS10:119
for r being Real st - (sqrt 2) < r & r < - 1 holds
sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1)))
proof end;

theorem :: SINCOS10:120
for r being Real st 1 < r & r < sqrt 2 holds
sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1))
proof end;

theorem Th121: :: SINCOS10:121
arcsec1 is_differentiable_on sec .: ].0,(PI / 2).[
proof end;

theorem Th122: :: SINCOS10:122
arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[
proof end;

theorem Th123: :: SINCOS10:123
arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0.[
proof end;

theorem Th124: :: SINCOS10:124
arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[
proof end;

theorem :: SINCOS10:125
sec .: ].0,(PI / 2).[ is open
proof end;

theorem :: SINCOS10:126
sec .: ].(PI / 2),PI.[ is open
proof end;

theorem :: SINCOS10:127
cosec .: ].(- (PI / 2)),0.[ is open
proof end;

theorem :: SINCOS10:128
cosec .: ].0,(PI / 2).[ is open
proof end;

theorem :: SINCOS10:129
arcsec1 | (sec .: ].0,(PI / 2).[) is continuous by Th121, FDIFF_1:25;

theorem :: SINCOS10:130
arcsec2 | (sec .: ].(PI / 2),PI.[) is continuous by Th122, FDIFF_1:25;

theorem :: SINCOS10:131
arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is continuous by Th123, FDIFF_1:25;

theorem :: SINCOS10:132
arccosec2 | (cosec .: ].0,(PI / 2).[) is continuous by Th124, FDIFF_1:25;