:: SIN_COS9 semantic presentation

theorem Th1: :: SIN_COS9:1

].(- (PI / 2)),(PI / 2).[ c= dom tan

proof end;

theorem Th2: :: SIN_COS9:2

].0 ,PI .[ c= dom cot

proof end;

Lm1: tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[

proof end;

Lm2: cot is_differentiable_on ].0 ,PI .[

proof end;

Lm3: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff tan ,x = 1 / ((cos . x) ^2 )

proof end;

Lm4: for x being Real st x in ].0 ,PI .[ holds
diff cot ,x = - (1 / ((sin . x) ^2 ))

proof end;

theorem :: SIN_COS9:3

( tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ & ( for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff tan ,x = 1 / ((cos . x) ^2 ) ) ) by Lm1, Lm3;

theorem :: SIN_COS9:4

( cot is_differentiable_on ].0 ,PI .[ & ( for x being Real st x in ].0 ,PI .[ holds
diff cot ,x = - (1 / ((sin . x) ^2 )) ) ) by Lm2, Lm4;

theorem :: SIN_COS9:5

tan is_continuous_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_1:33;

theorem :: SIN_COS9:6

cot is_continuous_on ].0 ,PI .[ by Lm2, FDIFF_1:33;

theorem Th7: :: SIN_COS9:7

tan is_increasing_on ].(- (PI / 2)),(PI / 2).[

proof end;

theorem Th8: :: SIN_COS9:8

cot is_decreasing_on ].0 ,PI .[

proof end;

theorem :: SIN_COS9:9

tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:16;

theorem :: SIN_COS9:10

cot | ].0 ,PI .[ is one-to-one by Th8, FCONT_3:16;

registration

cluster K7(tan ,].(- (PI / 2)),(PI / 2).[) -> one-to-one ;
coherence by Th7, FCONT_3:16;
cluster K7(cot ,].0 ,PI .[) -> one-to-one ;
coherence by Th8, FCONT_3:16;

end;

definition

func arctan -> PartFunc of REAL , REAL equals :: SIN_COS9:def 1
(tan | ].(- (PI / 2)),(PI / 2).[) " ;
coherence ;
func arccot -> PartFunc of REAL , REAL equals :: SIN_COS9:def 2
(cot | ].0 ,PI .[) " ;
coherence ;

end;

:: deftheorem defines arctan SIN_COS9:def 1 :

:: deftheorem defines arccot SIN_COS9:def 2 :

definition

let r be Real;
func arctan r -> set equals :: SIN_COS9:def 3
arctan . r;
coherence ;
func arccot r -> set equals :: SIN_COS9:def 4
arccot . r;
coherence ;

end;

:: deftheorem defines arctan SIN_COS9:def 3 :

:: deftheorem defines arccot SIN_COS9:def 4 :

definition

let r be Real;
:: original: arctan
redefine func arctan r -> Real;
coherence ;
:: original: arccot
redefine func arccot r -> Real;
coherence ;

end;

Lm5: arctan " = tan | ].(- (PI / 2)),(PI / 2).[
by FUNCT_1:65;

Lm6: arccot " = cot | ].0 ,PI .[
by FUNCT_1:65;

theorem Th11: :: SIN_COS9:11

rng arctan = ].(- (PI / 2)),(PI / 2).[

proof end;

theorem Th12: :: SIN_COS9:12

rng arccot = ].0 ,PI .[

proof end;

registration

cluster arctan -> one-to-one ;
coherence ;
cluster arccot -> one-to-one ;
coherence ;

end;

definition

let th be Real;
:: original: tan
redefine func tan th -> Real;
coherence ;
:: original: cot
redefine func cot th -> Real;
coherence ;

end;

Lm7: - (PI / 4) in ].(- (PI / 2)),(PI / 2).[

proof end;

Lm8: PI / 4 in ].(- (PI / 2)),(PI / 2).[

proof end;

Lm9: PI / 4 in ].0 ,PI .[

proof end;

Lm10: (3 / 4) * PI in ].0 ,PI .[

proof end;

Lm11: dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).]

proof end;

Lm12: dom (cot | [.(PI / 4),((3 / 4) * PI ).]) = [.(PI / 4),((3 / 4) * PI ).]

proof end;

theorem Th13: :: SIN_COS9:13

for x being real number st x in ].(- (PI / 2)),(PI / 2).[ holds
tan . x = tan x

proof end;

theorem Th14: :: SIN_COS9:14

for x being real number st x in ].0 ,PI .[ holds
cot . x = cot x

proof end;

theorem :: SIN_COS9:15

for x being Real st cos . x <> 0 holds
tan . x = tan x

proof end;

theorem :: SIN_COS9:16

for x being Real st sin . x <> 0 holds
cot . x = cot x

proof end;

theorem Th15: :: SIN_COS9:17

( tan . (- (PI / 4)) = - 1 & tan (- (PI / 4)) = - 1 )

proof end;

theorem Th16: :: SIN_COS9:18

( cot . (PI / 4) = 1 & cot (PI / 4) = 1 & cot . ((3 / 4) * PI ) = - 1 & cot ((3 / 4) * PI ) = - 1 )

proof end;

theorem Th17: :: SIN_COS9:19

for x being set st x in [.(- (PI / 4)),(PI / 4).] holds
tan . x in [.(- 1),1.]

proof end;

theorem Th18: :: SIN_COS9:20

for x being set st x in [.(PI / 4),((3 / 4) * PI ).] holds
cot . x in [.(- 1),1.]

proof end;

theorem Th19: :: SIN_COS9:21

rng (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- 1),1.]

proof end;

theorem Th20: :: SIN_COS9:22

rng (cot | [.(PI / 4),((3 / 4) * PI ).]) = [.(- 1),1.]

proof end;

theorem Th21: :: SIN_COS9:23

[.(- 1),1.] c= dom arctan

proof end;

theorem Th22: :: SIN_COS9:24

[.(- 1),1.] c= dom arccot

proof end;

Lm13: tan | [.(- (PI / 4)),(PI / 4).] is_increasing_on [.(- (PI / 4)),(PI / 4).]

proof end;

Lm14: cot | [.(PI / 4),((3 / 4) * PI ).] is_decreasing_on [.(PI / 4),((3 / 4) * PI ).]

proof end;

Lm15: tan | [.(- (PI / 4)),(PI / 4).] is one-to-one

proof end;

Lm16: cot | [.(PI / 4),((3 / 4) * PI ).] is one-to-one

proof end;

registration

cluster K7(tan ,[.(- (PI / 4)),(PI / 4).]) -> one-to-one ;
coherence by Lm15;
cluster K7(cot ,[.(PI / 4),((3 / 4) * PI ).]) -> one-to-one ;
coherence by Lm16;

end;

theorem Th23: :: SIN_COS9:25

arctan | [.(- 1),1.] = (tan | [.(- (PI / 4)),(PI / 4).]) "

proof end;

theorem Th24: :: SIN_COS9:26

arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI ).]) "

proof end;

theorem :: SIN_COS9:27

(tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by Th19, Th23, FUNCT_1:61;

theorem :: SIN_COS9:28

(cot | [.(PI / 4),((3 / 4) * PI ).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by Th20, Th24, FUNCT_1:61;

theorem :: SIN_COS9:29

(tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by Th19, Th23, FUNCT_1:61;

theorem :: SIN_COS9:30

(cot | [.(PI / 4),((3 / 4) * PI ).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by Th20, Th24, FUNCT_1:61;

theorem Th29: :: SIN_COS9:31

arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by Lm5, Th11, FUNCT_1:61;

theorem Th30: :: SIN_COS9:32

arccot * (cot | ].0 ,PI .[) = id ].0 ,PI .[ by Lm6, Th12, FUNCT_1:61;

theorem :: SIN_COS9:33

arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by Lm5, Th11, FUNCT_1:61;

theorem :: SIN_COS9:34

arccot * (cot | ].0 ,PI .[) = id ].0 ,PI .[ by Lm6, Th12, FUNCT_1:61;

theorem Th33: :: SIN_COS9:35

for r being Real st - (PI / 2) < r & r < PI / 2 holds
( arctan (tan . r) = r & arctan (tan r) = r )

proof end;

theorem Th34: :: SIN_COS9:36

for r being Real st 0 < r & r < PI holds
( arccot (cot . r) = r & arccot (cot r) = r )

proof end;

theorem Th35: :: SIN_COS9:37

( arctan (- 1) = - (PI / 4) & arctan . (- 1) = - (PI / 4) )

proof end;

theorem Th36: :: SIN_COS9:38

( arccot (- 1) = (3 / 4) * PI & arccot . (- 1) = (3 / 4) * PI )

proof end;

theorem Th37: :: SIN_COS9:39

( arctan 1 = PI / 4 & arctan . 1 = PI / 4 )

proof end;

theorem Th38: :: SIN_COS9:40

( arccot 1 = PI / 4 & arccot . 1 = PI / 4 )

proof end;

theorem Th39: :: SIN_COS9:41

( tan . 0 = 0 & tan 0 = 0 )

proof end;

theorem Th40: :: SIN_COS9:42

( cot . (PI / 2) = 0 & cot (PI / 2) = 0 )

proof end;

theorem :: SIN_COS9:43

( arctan 0 = 0 & arctan . 0 = 0 )

proof end;

theorem :: SIN_COS9:44

( arccot 0 = PI / 2 & arccot . 0 = PI / 2 )

proof end;

theorem Th43: :: SIN_COS9:45

arctan is_increasing_on tan .: ].(- (PI / 2)),(PI / 2).[

proof end;

theorem Th44: :: SIN_COS9:46

arccot is_decreasing_on cot .: ].0 ,PI .[

proof end;

theorem Th45: :: SIN_COS9:47

arctan is_increasing_on [.(- 1),1.]

proof end;

theorem Th46: :: SIN_COS9:48

arccot is_decreasing_on [.(- 1),1.]

proof end;

theorem Th47: :: SIN_COS9:49

for x being set st x in [.(- 1),1.] holds
arctan . x in [.(- (PI / 4)),(PI / 4).]

proof end;

theorem Th48: :: SIN_COS9:50

for x being set st x in [.(- 1),1.] holds
arccot . x in [.(PI / 4),((3 / 4) * PI ).]

proof end;

theorem Th49: :: SIN_COS9:51

for r being Real st - 1 <= r & r <= 1 holds
tan (arctan r) = r

proof end;

theorem Th50: :: SIN_COS9:52

for r being Real st - 1 <= r & r <= 1 holds
cot (arccot r) = r

proof end;

theorem Th51: :: SIN_COS9:53

arctan is_continuous_on [.(- 1),1.]

proof end;

theorem Th52: :: SIN_COS9:54

arccot is_continuous_on [.(- 1),1.]

proof end;

theorem Th53: :: SIN_COS9:55

rng (arctan | [.(- 1),1.]) = [.(- (PI / 4)),(PI / 4).]

proof end;

theorem Th54: :: SIN_COS9:56

rng (arccot | [.(- 1),1.]) = [.(PI / 4),((3 / 4) * PI ).]

proof end;

theorem :: SIN_COS9:57

for r being Real st - 1 <= r & r <= 1 & arctan r = - (PI / 4) holds
r = - 1 by Th49, Th15;

theorem :: SIN_COS9:58

for r being Real st - 1 <= r & r <= 1 & arccot r = (3 / 4) * PI holds
r = - 1 by Th50, Th16;

theorem :: SIN_COS9:59

for r being Real st - 1 <= r & r <= 1 & arctan r = 0 holds
r = 0 by Th49, Th39;

theorem :: SIN_COS9:60

for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 2 holds
r = 0 by Th40, Th50;

theorem :: SIN_COS9:61

for r being Real st - 1 <= r & r <= 1 & arctan r = PI / 4 holds
r = 1

proof end;

theorem :: SIN_COS9:62

for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 4 holds
r = 1 by Th16, Th50;

theorem Th61: :: SIN_COS9:63

for r being Real st - 1 <= r & r <= 1 holds
( - (PI / 4) <= arctan r & arctan r <= PI / 4 )

proof end;

theorem Th62: :: SIN_COS9:64

for r being Real st - 1 <= r & r <= 1 holds
( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI )

proof end;

theorem :: SIN_COS9:65

for r being Real st - 1 < r & r < 1 holds
( - (PI / 4) < arctan r & arctan r < PI / 4 )

proof end;

theorem :: SIN_COS9:66

for r being Real st - 1 < r & r < 1 holds
( PI / 4 < arccot r & arccot r < (3 / 4) * PI )

proof end;

theorem :: SIN_COS9:67

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

proof end;

theorem :: SIN_COS9:68

for r being Real st - 1 <= r & r <= 1 holds
arccot r = PI - (arccot (- r))

proof end;

theorem :: SIN_COS9:69

for r being Real st - 1 <= r & r <= 1 holds
cot (arctan r) = 1 / r

proof end;

theorem :: SIN_COS9:70

for r being Real st - 1 <= r & r <= 1 holds
tan (arccot r) = 1 / r

proof end;

theorem Th69: :: SIN_COS9:71