:: SINCOS10 semantic presentation

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 is_continuous_on ].0 ,(PI / 2).[ by Th5, FDIFF_1:33;

theorem :: SINCOS10:10
sec is_continuous_on ].(PI / 2),PI .[ by Th6, FDIFF_1:33;

theorem :: SINCOS10:11
cosec is_continuous_on ].(- (PI / 2)),0 .[ by Th7, FDIFF_1:33;

theorem :: SINCOS10:12
cosec is_continuous_on ].0 ,(PI / 2).[ by Th8, FDIFF_1:33;

theorem Th13: :: SINCOS10:13
sec is_increasing_on ].0 ,(PI / 2).[
proof end;

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

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

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

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

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

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

theorem Th20: :: SINCOS10:20
cosec is_decreasing_on ].0 ,(PI / 2).]
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 K7(sec ,[.0 ,(PI / 2).[) -> one-to-one ;
coherence
sec | [.0 ,(PI / 2).[ is one-to-one by Th17, FCONT_3:16;
cluster K7(sec ,].(PI / 2),PI .]) -> one-to-one ;
coherence
sec | ].(PI / 2),PI .] is one-to-one by Th18, FCONT_3:16;
cluster K7(cosec ,[.(- (PI / 2)),0 .[) -> one-to-one ;
coherence
cosec | [.(- (PI / 2)),0 .[ is one-to-one by Th19, FCONT_3:16;
cluster K7(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;

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

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

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

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

definition
let th be real number ;
:: original: sec
redefine func sec th -> Real;
coherence
sec th is Real ;
:: original: cosec
redefine func cosec th -> Real;
coherence
cosec th is Real ;
end;

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

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

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

Lm12: ( PI / 4 in ].0 ,(PI / 2).] & PI / 2 in ].0 ,(PI / 2).] )
proof 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;

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

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

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

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

Lm17: ( 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;

Lm18: ( 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;

Lm19: ( 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;

Lm20: ( 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 is_continuous_on [.0 ,(PI / 2).[
proof end;

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

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

theorem Th40: :: SINCOS10:40
cosec is_continuous_on ].0 ,(PI / 2).]
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;

Lm21: sec | [.0 ,(PI / 4).] is_increasing_on [.0 ,(PI / 4).]
proof end;

Lm22: sec | [.((3 / 4) * PI ),PI .] is_increasing_on [.((3 / 4) * PI ),PI .]
proof end;

Lm23: cosec | [.(- (PI / 2)),(- (PI / 4)).] is_decreasing_on [.(- (PI / 2)),(- (PI / 4)).]
proof end;

Lm24: cosec | [.(PI / 4),(PI / 2).] is_decreasing_on [.(PI / 4),(PI / 2).]
proof end;

Lm25: sec