:: SIN_COS5 semantic presentation

theorem Th1: :: SIN_COS5:1

for b₁ being real number st cos b₁ <> 0 holds
cosec b₁ = (sec b₁) / (tan b₁)

proof end;

theorem Th2: :: SIN_COS5:2

for b₁ being real number st sin b₁ <> 0 holds
cos b₁ = (sin b₁) * (cot b₁)

proof end;

theorem Th3: :: SIN_COS5:3

for b₁, b₂, b₃ being real number st sin b₁ <> 0 & sin b₂ <> 0 & sin b₃ <> 0 holds
sin ((b₁ + b₂) + b₃) = (((sin b₁) * (sin b₂)) * (sin b₃)) * (((((cot b₂) * (cot b₃)) + ((cot b₁) * (cot b₃))) + ((cot b₁) * (cot b₂))) - 1)

proof end;

theorem Th4: :: SIN_COS5:4

for b₁, b₂, b₃ being real number st sin b₁ <> 0 & sin b₂ <> 0 & sin b₃ <> 0 holds
cos ((b₁ + b₂) + b₃) = - ((((sin b₁) * (sin b₂)) * (sin b₃)) * ((((cot b₁) + (cot b₂)) + (cot b₃)) - (((cot b₁) * (cot b₂)) * (cot b₃))))

proof end;

theorem Th5: :: SIN_COS5:5

for b₁ being real number holds sin (2 * b₁) = (2 * (sin b₁)) * (cos b₁)

proof end;

theorem Th6: :: SIN_COS5:6

for b₁ being real number st cos b₁ <> 0 holds
sin (2 * b₁) = (2 * (tan b₁)) / (1 + ((tan b₁) ^2 ))

proof end;

theorem Th7: :: SIN_COS5:7

for b₁ being real number holds
( cos (2 * b₁) = ((cos b₁) ^2 ) - ((sin b₁) ^2 ) & cos (2 * b₁) = (2 * ((cos b₁) ^2 )) - 1 & cos (2 * b₁) = 1 - (2 * ((sin b₁) ^2 )) )

proof end;

theorem Th8: :: SIN_COS5:8

for b₁ being real number st cos b₁ <> 0 holds
cos (2 * b₁) = (1 - ((tan b₁) ^2 )) / (1 + ((tan b₁) ^2 ))

proof end;

theorem Th9: :: SIN_COS5:9

for b₁ being real number st cos b₁ <> 0 holds
tan (2 * b₁) = (2 * (tan b₁)) / (1 - ((tan b₁) ^2 ))

proof end;

theorem Th10: :: SIN_COS5:10

for b₁ being real number st sin b₁ <> 0 holds
cot (2 * b₁) = (((cot b₁) ^2 ) - 1) / (2 * (cot b₁))

proof end;

theorem Th11: :: SIN_COS5:11

for b₁ being real number st cos b₁ <> 0 holds
(sec b₁) ^2 = 1 + ((tan b₁) ^2 )

proof end;

theorem Th12: :: SIN_COS5:12

for b₁ being real number holds cot b₁ = 1 / (tan b₁)

proof end;

theorem Th13: :: SIN_COS5:13

for b₁ being real number st cos b₁ <> 0 & sin b₁ <> 0 holds
( sec (2 * b₁) = ((sec b₁) ^2 ) / (1 - ((tan b₁) ^2 )) & sec (2 * b₁) = ((cot b₁) + (tan b₁)) / ((cot b₁) - (tan b₁)) )

proof end;

theorem Th14: :: SIN_COS5:14

for b₁ being real number st sin b₁ <> 0 holds
(cosec b₁) ^2 = 1 + ((cot b₁) ^2 )

proof end;

theorem Th15: :: SIN_COS5:15

for b₁ being real number st cos b₁ <> 0 & sin b₁ <> 0 holds
( cosec (2 * b₁) = ((sec b₁) * (cosec b₁)) / 2 & cosec (2 * b₁) = ((tan b₁) + (cot b₁)) / 2 )

proof end;

theorem Th16: :: SIN_COS5:16

for b₁ being real number holds sin (3 * b₁) = (- (4 * ((sin b₁) |^ 3))) + (3 * (sin b₁))

proof end;

theorem Th17: :: SIN_COS5:17

for b₁ being real number holds cos (3 * b₁) = (4 * ((cos b₁) |^ 3)) - (3 * (cos b₁))

proof end;

theorem Th18: :: SIN_COS5:18

for b₁ being real number st cos b₁ <> 0 holds
tan (3 * b₁) = ((3 * (tan b₁)) - ((tan b₁) |^ 3)) / (1 - (3 * ((tan b₁) ^2 )))

proof end;

theorem Th19: :: SIN_COS5:19

for b₁ being real number st sin b₁ <> 0 holds
cot (3 * b₁) = (((cot b₁) |^ 3) - (3 * (cot b₁))) / ((3 * ((cot b₁) ^2 )) - 1)

proof end;

theorem Th20: :: SIN_COS5:20

for b₁ being real number holds (sin b₁) ^2 = (1 - (cos (2 * b₁))) / 2

proof end;

theorem Th21: :: SIN_COS5:21

for b₁ being real number holds (cos b₁) ^2 = (1 + (cos (2 * b₁))) / 2

proof end;

theorem Th22: :: SIN_COS5:22

for b₁ being real number holds (sin b₁) |^ 3 = ((3 * (sin b₁)) - (sin (3 * b₁))) / 4

proof end;

theorem Th23: :: SIN_COS5:23

for b₁ being real number holds (cos b₁) |^ 3 = ((3 * (cos b₁)) + (cos (3 * b₁))) / 4

proof end;

theorem Th24: :: SIN_COS5:24

for b₁ being real number holds (sin b₁) |^ 4 = ((3 - (4 * (cos (2 * b₁)))) + (cos (4 * b₁))) / 8

proof end;

theorem Th25: :: SIN_COS5:25

for b₁ being real number holds (cos b₁) |^ 4 = ((3 + (4 * (cos (2 * b₁)))) + (cos (4 * b₁))) / 8

proof end;

theorem Th26: :: SIN_COS5:26

for b₁ being real number holds
( sin (b₁ / 2) = sqrt ((1 - (cos b₁)) / 2) or sin (b₁ / 2) = - (sqrt ((1 - (cos b₁)) / 2)) )

proof end;

theorem Th27: :: SIN_COS5:27

for b₁ being real number holds
( cos (b₁ / 2) = sqrt ((1 + (cos b₁)) / 2) or cos (b₁ / 2) = - (sqrt ((1 + (cos b₁)) / 2)) )

proof end;

theorem Th28: :: SIN_COS5:28

for b₁ being real number st sin (b₁ / 2) <> 0 holds
tan (b₁ / 2) = (1 - (cos b₁)) / (sin b₁)

proof end;

theorem Th29: :: SIN_COS5:29

for b₁ being real number st cos (b₁ / 2) <> 0 holds
tan (b₁ / 2) = (sin b₁) / (1 + (cos b₁))

proof end;

theorem Th30: :: SIN_COS5:30

for b₁ being real number holds
( tan (b₁ / 2) = sqrt ((1 - (cos b₁)) / (1 + (cos b₁))) or tan (b₁ / 2) = - (sqrt ((1 - (cos b₁)) / (1 + (cos b₁)))) )

proof end;

theorem Th31: :: SIN_COS5:31

for b₁ being real number st cos (b₁ / 2) <> 0 holds
cot (b₁ / 2) = (1 + (cos b₁)) / (sin b₁)

proof end;

theorem Th32: :: SIN_COS5:32

for b₁ being real number st sin (b₁ / 2) <> 0 holds
cot (b₁ / 2) = (sin b₁) / (1 - (cos b₁))

proof end;

theorem Th33: :: SIN_COS5:33

for b₁ being real number holds
( cot (b₁ / 2) = sqrt ((1 + (cos b₁)) / (1 - (cos b₁))) or cot (b₁ / 2) = - (sqrt ((1 + (cos b₁)) / (1 - (cos b₁)))) )

proof end;

theorem Th34: :: SIN_COS5:34

for b₁ being real number st sin (b₁ / 2) <> 0 & cos (b₁ / 2) <> 0 & 1 - ((tan (b₁ / 2)) ^2 ) <> 0 & not sec (b₁ / 2) = sqrt ((2 * (sec b₁)) / ((sec b₁) + 1)) holds
sec (b₁ / 2) = - (sqrt ((2 * (sec b₁)) / ((sec b₁) + 1)))

proof end;

theorem Th35: :: SIN_COS5:35

for b₁ being real number st sin (b₁ / 2) <> 0 & cos (b₁ / 2) <> 0 & 1 - ((tan (b₁ / 2)) ^2 ) <> 0 & not cosec (b₁ / 2) = sqrt ((2 * (sec b₁)) / ((sec b₁) - 1)) holds
cosec (b₁ / 2) = - (sqrt ((2 * (sec b₁)) / ((sec b₁) - 1)))

proof end;

definition

let c₁ be real number ;
func coth c₁ -> Real equals :: SIN_COS5:def 1
(cosh a₁) / (sinh a₁);
coherence ;
func sech c₁ -> Real equals :: SIN_COS5:def 2
1 / (cosh a₁);
coherence ;
func cosech c₁ -> Real equals :: SIN_COS5:def 3
1 / (sinh a₁);
coherence ;

end;

:: deftheorem Def1 defines coth SIN_COS5:def 1 :

:: deftheorem Def2 defines sech SIN_COS5:def 2 :

:: deftheorem Def3 defines cosech SIN_COS5:def 3 :

theorem Th36: :: SIN_COS5:36

for b₁ being real number holds
( coth b₁ = ((exp b₁) + (exp (- b₁))) / ((exp b₁) - (exp (- b₁))) & sech b₁ = 2 / ((exp b₁) + (exp (- b₁))) & cosech b₁ = 2 / ((exp b₁) - (exp (- b₁))) )

proof end;

theorem Th37: :: SIN_COS5:37

for b₁ being real number st (exp b₁) - (exp (- b₁)) <> 0 holds
(tanh b₁) * (coth b₁) = 1

proof end;

theorem Th38: :: SIN_COS5:38

for b₁ being real number holds ((sech b₁) ^2 ) + ((tanh b₁) ^2 ) = 1

proof end;

theorem Th39: :: SIN_COS5:39

for b₁ being real number st sinh b₁ <> 0 holds
((coth b₁) ^2 ) - ((cosech b₁) ^2 ) = 1

proof end;

Lemma13: for b₁ being real number holds coth (- b₁) = - (coth b₁)

proof end;

theorem Th40: :: SIN_COS5:40

for b₁, b₂ being real number st sinh b₁ <> 0 & sinh b₂ <> 0 holds
coth (b₁ + b₂) = (1 + ((coth b₁) * (coth b₂))) / ((coth b₁) + (coth b₂))

proof end;

theorem Th41: :: SIN_COS5:41

for b₁, b₂ being real number st sinh b₁ <> 0 & sinh b₂ <> 0 holds
coth (b₁ - b₂) = (1 - ((coth b₁) * (coth b₂))) / ((coth b₁) - (coth b₂))

proof end;

theorem Th42: :: SIN_COS5:42

for b₁, b₂ being real number st sinh b₁ <> 0 & sinh b₂ <> 0 holds
( (coth b₁) + (coth b₂) = (sinh (b₁ + b₂)) / ((sinh b₁) * (sinh b₂)) & (coth b₁) - (coth b₂) = - ((sinh (b₁ - b₂)) / ((sinh b₁) * (sinh b₂))) )

proof end;

Lemma15: for b₁ being real number holds (cosh . b₁) ^2 = 1 + ((sinh . b₁) ^2 )

proof end;

Lemma16: for b₁ being real number holds ((cosh . b₁) ^2 ) - 1 = (sinh . b₁) ^2

proof end;

theorem Th43: :: SIN_COS5:43

for b₁ being real number holds sinh (3 * b₁) = (3 * (sinh b₁)) + (4 * ((sinh b₁) |^ 3))

proof end;

theorem Th44: :: SIN_COS5:44

for b₁ being real number holds cosh (3 * b₁) = (4 * ((cosh b₁) |^ 3)) - (3 * (cosh b₁))

proof end;

theorem Th45: :: SIN_COS5:45

for b₁ being real number st sinh b₁ <> 0 holds
coth (2 * b₁) = (1 + ((coth b₁) ^2 )) / (2 * (coth b₁))

proof end;

Lemma17: for b₁ being real number st b₁ > 0 holds
sinh b₁ >= 0

proof end;

Lemma18: sinh 0 = 0
by SIN_COS2:def 2, SIN_COS2:16;

theorem Th46: :: SIN_COS5:46

for b₁ being real number st b₁ >= 0 holds
sinh b₁ >= 0

proof end;

theorem Th47: :: SIN_COS5:47

for b₁ being real number st b₁ <= 0 holds
sinh b₁ <= 0

proof end;

theorem Th48: :: SIN_COS5:48

for b₁ being real number holds cosh (b₁ / 2) = sqrt (((cosh b₁) + 1) / 2)

proof end;

theorem Th49: :: SIN_COS5:49

for b₁ being real number st sinh (b₁ / 2) <> 0 holds
tanh (b₁ / 2) = ((cosh b₁) - 1) / (sinh b₁)

proof end;

theorem Th50: :: SIN_COS5:50

for b₁ being real number st cosh (b₁ / 2) <> 0 holds
tanh (b₁ / 2) = (sinh b₁) / ((cosh b₁) + 1)

proof end;

theorem Th51: :: SIN_COS5:51

for b₁ being real number st sinh (b₁ / 2) <> 0 holds
coth (b₁ / 2) = (sinh b₁) / ((cosh b₁) - 1)

proof end;

theorem Th52: :: SIN_COS5:52

for b₁ being real number st cosh (b₁ / 2) <> 0 holds
coth (b₁ / 2) = ((cosh b₁) + 1) / (sinh b₁)

proof end;