:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2011 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:33;

theorem :: SINCOS10:10

sec | ].(PI / 2),PI.[ is continuous by Th6, FDIFF_1:33;

theorem :: SINCOS10:11

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

theorem :: SINCOS10:12

cosec | ].0,(PI / 2).[ is continuous by Th8, FDIFF_1:33;

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

then Lm21: ].0,(PI / 2).[ c= dom ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[)
by RELAT_1:103, XXREAL_1:22;

].(PI / 2),PI.[ = dom (sec | ].(PI / 2),PI.[)
by Lm11, Th2, RELAT_1:91, XBOOLE_1:1;

then Lm22: ].(PI / 2),PI.[ c= dom ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[)
by RELAT_1:103, XXREAL_1:21;

].(- (PI / 2)),0.[ = dom (cosec | ].(- (PI / 2)),0.[)
by Lm15, Th3, RELAT_1:91, XBOOLE_1:1;

then Lm23: ].(- (PI / 2)),0.[ c= dom ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[)
by RELAT_1:103, XXREAL_1:22;

].0,(PI / 2).[ = dom (cosec | ].0,(PI / 2).[)
by Lm17, Th4, RELAT_1:91, XBOOLE_1:1;

then Lm24: ].0,(PI / 2).[ c= dom ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[)
by RELAT_1:103, 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:16;

theorem :: SINCOS10:22

sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:16;

theorem :: SINCOS10:23

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

theorem :: SINCOS10:24

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

registration

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

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:65;

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

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

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

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 K79(sec,[.0,(PI / 4).]) -> one-to-one ;
coherence
sec | [.0,(PI / 4).] is one-to-one by Lm41;
cluster K79(sec,[.((3 / 4) * PI),PI.]) -> one-to-one ;
coherence
sec | [.((3 / 4) * PI),PI.] is one-to-one by Lm42;
cluster K79(cosec,[.(- (PI / 2)),(- (PI / 4)).]) -> one-to-one ;
coherence
cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one by Lm43;
cluster K79(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:61;

theorem :: SINCOS10:54

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

theorem :: SINCOS10:55

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

theorem :: SINCOS10:56

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

theorem :: SINCOS10:57

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

theorem :: SINCOS10:58

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

theorem :: SINCOS10:59

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

theorem :: SINCOS10:60

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

theorem :: SINCOS10:61

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

theorem :: SINCOS10:62

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

theorem :: SINCOS10:63

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

theorem :: SINCOS10:64

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

theorem Th65: :: SINCOS10:65

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

theorem Th66: :: SINCOS10:66

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

theorem Th67: :: SINCOS10:67

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

theorem Th68: :: SINCOS10:68

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

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:33;

theorem :: SINCOS10:130

arcsec2 | (sec .: ].(PI / 2),PI.[) is continuous by Th122, FDIFF_1:33;

theorem :: SINCOS10:131

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

theorem :: SINCOS10:132

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