:: by Bing Xie , Xiquan Liang and Fuguo Ge

::

:: Received March 18, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

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

proof end;

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

proof end;

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

proof end;

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

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) ) )

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) ) )

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)) ) )

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)) ) )

diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )

proof end;

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;

Lm11: ].(PI / 2),PI.[ c= ].(PI / 2),PI.]

by XXREAL_1:21;

then Lm12: ].(PI / 2),PI.[ c= dom sec

by Th2;

Lm13: [.0,(PI / 4).] c= [.0,(PI / 2).[

by Lm5, XXREAL_2:def 12;

Lm14: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.]

by Lm6, XXREAL_2:def 12;

Lm15: ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[

by XXREAL_1:22;

then Lm16: ].(- (PI / 2)),0.[ c= dom cosec

by Th3;

Lm17: ].0,(PI / 2).[ c= ].0,(PI / 2).]

by XXREAL_1:21;

then Lm18: ].0,(PI / 2).[ c= dom cosec

by Th4;

Lm19: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[

by Lm7, XXREAL_2:def 12;

Lm20: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).]

by Lm8, XXREAL_2:def 12;

].0,(PI / 2).[ = dom (sec | ].0,(PI / 2).[)

by Lm9, Th1, RELAT_1:62, XBOOLE_1:1;

then Lm21: ].0,(PI / 2).[ c= dom ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[)

by RELAT_1:74, XXREAL_1:22;

].(PI / 2),PI.[ = dom (sec | ].(PI / 2),PI.[)

by Lm11, Th2, RELAT_1:62, XBOOLE_1:1;

then Lm22: ].(PI / 2),PI.[ c= dom ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[)

by RELAT_1:74, XXREAL_1:21;

].(- (PI / 2)),0.[ = dom (cosec | ].(- (PI / 2)),0.[)

by Lm15, Th3, RELAT_1:62, XBOOLE_1:1;

then Lm23: ].(- (PI / 2)),0.[ c= dom ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[)

by RELAT_1:74, XXREAL_1:22;

].0,(PI / 2).[ = dom (cosec | ].0,(PI / 2).[)

by Lm17, Th4, RELAT_1:62, XBOOLE_1:1;

then Lm24: ].0,(PI / 2).[ c= dom ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[)

by RELAT_1:74, XXREAL_1:21;

registration

coherence

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

coherence

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

coherence

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

coherence

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

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

coherence

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

coherence

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

coherence

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

definition

coherence

(sec | [.0,(PI / 2).[) " is PartFunc of REAL,REAL ;

coherence

(sec | ].(PI / 2),PI.]) " is PartFunc of REAL,REAL ;

coherence

(cosec | [.(- (PI / 2)),0.[) " is PartFunc of REAL,REAL ;

coherence

(cosec | ].0,(PI / 2).]) " is PartFunc of REAL,REAL ;

end;
(sec | [.0,(PI / 2).[) " is PartFunc of REAL,REAL ;

coherence

(sec | ].(PI / 2),PI.]) " is PartFunc of REAL,REAL ;

coherence

(cosec | [.(- (PI / 2)),0.[) " is PartFunc of REAL,REAL ;

coherence

(cosec | ].0,(PI / 2).]) " is PartFunc of REAL,REAL ;

definition

let r be Real;

coherence

arcsec1 . r is set ;

coherence

arcsec2 . r is set ;

coherence

arccosec1 . r is set ;

coherence

arccosec2 . r is set ;

end;
coherence

arcsec1 . r is set ;

coherence

arcsec2 . r is set ;

coherence

arccosec1 . r is set ;

coherence

arccosec2 . r is set ;

:: deftheorem defines arccosec1 SINCOS10:def 7 :

for r being Real holds arccosec1 r = arccosec1 . r;

for r being Real holds arccosec1 r = arccosec1 . r;

:: deftheorem defines arccosec2 SINCOS10:def 8 :

for r being Real holds arccosec2 r = arccosec2 . r;

for r being Real holds arccosec2 r = arccosec2 . r;

registration

let r be Real;

coherence

arcsec1 r is real ;

coherence

arcsec2 r is real ;

coherence

arccosec1 r is real ;

coherence

arccosec2 r is real ;

end;
coherence

arcsec1 r is real ;

coherence

arcsec2 r is real ;

coherence

arccosec1 r is real ;

coherence

arccosec2 r is real ;

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;

registration

coherence

arcsec1 is one-to-one ;

coherence

arcsec2 is one-to-one ;

coherence

arccosec1 is one-to-one ;

coherence

arccosec2 is one-to-one ;

end;
arcsec1 is one-to-one ;

coherence

arcsec2 is one-to-one ;

coherence

arccosec1 is one-to-one ;

coherence

arccosec2 is one-to-one ;

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 Th32: :: SINCOS10:32

( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 )

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 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 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 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 st th in ].0,(PI / 2).] holds

(cosec | ].0,(PI / 2).]) . th = cosec . th ) )

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

coherence

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

coherence

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

coherence

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

coherence

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

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

coherence

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

coherence

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

coherence

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

theorem :: SINCOS10:53

theorem :: SINCOS10:54

theorem :: SINCOS10:55

theorem :: SINCOS10:56

theorem :: SINCOS10:57

theorem :: SINCOS10:58

theorem :: SINCOS10:59

theorem :: SINCOS10:60

theorem :: SINCOS10:61

theorem :: SINCOS10:62

theorem :: SINCOS10:63

theorem :: SINCOS10:64

theorem :: SINCOS10:101

theorem :: SINCOS10:102

theorem :: SINCOS10:103

theorem :: SINCOS10:104

theorem Th106: :: SINCOS10:106

for r being Real st - (sqrt 2) <= r & r <= - 1 holds

( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI )

( (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) )

( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) )

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) )

( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) )

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 )

( 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 )

( 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) )

( 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 )

( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r )

proof end;

theorem :: SINCOS10:118

for r being Real st - (sqrt 2) < r & r < - 1 holds

cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1)))

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)))

sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1)))

proof end;

theorem :: SINCOS10:131