:: SIN_COS8 semantic presentation

Lemma1: for b₁ being real number holds
( cosh b₁ >= 1 & cosh 0 = 1 & sinh 0 = 0 )

proof end;

Lemma2: for b₁ being real number st b₁ >= 0 holds
sinh b₁ >= 0
by SIN_COS5:46;

Lemma3: for b₁ being real number holds
( sinh b₁ = ((exp b₁) - (exp (- b₁))) / 2 & cosh b₁ = ((exp b₁) + (exp (- b₁))) / 2 & tanh b₁ = ((exp b₁) - (exp (- b₁))) / ((exp b₁) + (exp (- b₁))) )

proof end;

Lemma4: for b₁ being real number holds
( ((cosh b₁) ^2 ) - ((sinh b₁) ^2 ) = 1 & ((cosh b₁) * (cosh b₁)) - ((sinh b₁) * (sinh b₁)) = 1 )

proof end;

theorem Th1: :: SIN_COS8:1

for b₁ being real number holds
( tanh b₁ = (sinh b₁) / (cosh b₁) & tanh 0 = 0 )

proof end;

Lemma6: for b₁ being real number st b₁ <> 0 holds
( sinh b₁ <> 0 & tanh b₁ <> 0 )

proof end;

Lemma7: for b₁, b₂ being real number st b₁ - b₂ <> 0 holds
sinh ((b₁ / 2) - (b₂ / 2)) <> 0

proof end;

Lemma8: for b₁, b₂ being real number st b₁ + b₂ <> 0 holds
sinh ((b₁ / 2) + (b₂ / 2)) <> 0

proof end;

Lemma9: for b₁ being real number holds
( (sinh b₁) ^2 = (1 / 2) * ((cosh (2 * b₁)) - 1) & (cosh b₁) ^2 = (1 / 2) * ((cosh (2 * b₁)) + 1) )

proof end;

Lemma10: for b₁ being real number holds
( sinh (- b₁) = - (sinh b₁) & cosh (- b₁) = cosh b₁ & tanh (- b₁) = - (tanh b₁) & coth (- b₁) = - (coth b₁) & sech (- b₁) = sech b₁ & cosech (- b₁) = - (cosech b₁) )

proof end;

theorem Th2: :: SIN_COS8:2

for b₁ being real number holds
( sinh b₁ = 1 / (cosech b₁) & cosh b₁ = 1 / (sech b₁) & tanh b₁ = 1 / (coth b₁) )

proof end;

Lemma12: for b₁ being real number holds (exp b₁) + (exp (- b₁)) >= 2

proof end;

theorem Th3: :: SIN_COS8:3

for b₁ being real number holds
( sech b₁ <= 1 & 0 < sech b₁ & sech 0 = 1 )

proof end;

theorem Th4: :: SIN_COS8:4

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

proof end;

theorem Th5: :: SIN_COS8:5

for b₁ being real number holds
( cosh b₁ = 1 / (sqrt (1 - ((tanh b₁) ^2 ))) & sinh b₁ = (tanh b₁) / (sqrt (1 - ((tanh b₁) ^2 ))) )

proof end;

theorem Th6: :: SIN_COS8:6

for b₁ being real number
for b₂ being Nat holds
( ((cosh b₁) + (sinh b₁)) |^ b₂ = (cosh (b₂ * b₁)) + (sinh (b₂ * b₁)) & ((cosh b₁) - (sinh b₁)) |^ b₂ = (cosh (b₂ * b₁)) - (sinh (b₂ * b₁)) )

proof end;

theorem Th7: :: SIN_COS8:7

for b₁ being real number holds
( exp b₁ = (cosh b₁) + (sinh b₁) & exp (- b₁) = (cosh b₁) - (sinh b₁) & exp b₁ = ((cosh (b₁ / 2)) + (sinh (b₁ / 2))) / ((cosh (b₁ / 2)) - (sinh (b₁ / 2))) & exp (- b₁) = ((cosh (b₁ / 2)) - (sinh (b₁ / 2))) / ((cosh (b₁ / 2)) + (sinh (b₁ / 2))) & exp b₁ = (1 + (tanh (b₁ / 2))) / (1 - (tanh (b₁ / 2))) & exp (- b₁) = (1 - (tanh (b₁ / 2))) / (1 + (tanh (b₁ / 2))) )

proof end;

theorem Th8: :: SIN_COS8:8

for b₁ being real number st b₁ <> 0 holds
( exp b₁ = ((coth (b₁ / 2)) + 1) / ((coth (b₁ / 2)) - 1) & exp (- b₁) = ((coth (b₁ / 2)) - 1) / ((coth (b₁ / 2)) + 1) )

proof end;

theorem Th9: :: SIN_COS8:9

for b₁ being real number holds ((cosh b₁) + (sinh b₁)) / ((cosh b₁) - (sinh b₁)) = (1 + (tanh b₁)) / (1 - (tanh b₁))

proof end;

Lemma15: for b₁, b₂ being real number holds
( cosh (b₁ + b₂) = ((cosh b₁) * (cosh b₂)) + ((sinh b₁) * (sinh b₂)) & cosh (b₁ - b₂) = ((cosh b₁) * (cosh b₂)) - ((sinh b₁) * (sinh b₂)) & sinh (b₁ + b₂) = ((sinh b₁) * (cosh b₂)) + ((cosh b₁) * (sinh b₂)) & sinh (b₁ - b₂) = ((sinh b₁) * (cosh b₂)) - ((cosh b₁) * (sinh b₂)) & tanh (b₁ + b₂) = ((tanh b₁) + (tanh b₂)) / (1 + ((tanh b₁) * (tanh b₂))) & tanh (b₁ - b₂) = ((tanh b₁) - (tanh b₂)) / (1 - ((tanh b₁) * (tanh b₂))) )

proof end;

theorem Th10: :: SIN_COS8:10

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

proof end;

theorem Th11: :: SIN_COS8:11

for b₁, b₂ being real number holds
( (sinh b₁) * (sinh b₂) = (1 / 2) * ((cosh (b₁ + b₂)) - (cosh (b₁ - b₂))) & (sinh b₁) * (cosh b₂) = (1 / 2) * ((sinh (b₁ + b₂)) + (sinh (b₁ - b₂))) & (cosh b₁) * (sinh b₂) = (1 / 2) * ((sinh (b₁ + b₂)) - (sinh (b₁ - b₂))) & (cosh b₁) * (cosh b₂) = (1 / 2) * ((cosh (b₁ + b₂)) + (cosh (b₁ - b₂))) )

proof end;

theorem Th12: :: SIN_COS8:12

for b₁, b₂ being real number holds ((sinh b₁) ^2 ) - ((cosh b₂) ^2 ) = ((sinh (b₁ + b₂)) * (sinh (b₁ - b₂))) - 1

proof end;

Lemma17: for b₁, b₂ being real number holds
( (sinh b₁) + (sinh b₂) = (2 * (sinh ((b₁ / 2) + (b₂ / 2)))) * (cosh ((b₁ / 2) - (b₂ / 2))) & (sinh b₁) - (sinh b₂) = (2 * (sinh ((b₁ / 2) - (b₂ / 2)))) * (cosh ((b₁ / 2) + (b₂ / 2))) & (cosh b₁) + (cosh b₂) = (2 * (cosh ((b₁ / 2) + (b₂ / 2)))) * (cosh ((b₁ / 2) - (b₂ / 2))) & (cosh b₁) - (cosh b₂) = (2 * (sinh ((b₁ / 2) - (b₂ / 2)))) * (sinh ((b₁ / 2) + (b₂ / 2))) & (tanh b₁) + (tanh b₂) = (sinh (b₁ + b₂)) / ((cosh b₁) * (cosh b₂)) & (tanh b₁) - (tanh b₂) = (sinh (b₁ - b₂)) / ((cosh b₁) * (cosh b₂)) )

proof end;

theorem Th13: :: SIN_COS8:13

for b₁, b₂ being real number holds
( (((sinh b₁) - (sinh b₂)) ^2 ) - (((cosh b₁) - (cosh b₂)) ^2 ) = 4 * ((sinh ((b₁ - b₂) / 2)) ^2 ) & (((cosh b₁) + (cosh b₂)) ^2 ) - (((sinh b₁) + (sinh b₂)) ^2 ) = 4 * ((cosh ((b₁ - b₂) / 2)) ^2 ) )

proof end;

theorem Th14: :: SIN_COS8:14

for b₁, b₂ being real number holds ((sinh b₁) + (sinh b₂)) / ((sinh b₁) - (sinh b₂)) = (tanh ((b₁ + b₂) / 2)) * (coth ((b₁ - b₂) / 2))

proof end;

theorem Th15: :: SIN_COS8:15

for b₁, b₂ being real number holds ((cosh b₁) + (cosh b₂)) / ((cosh b₁) - (cosh b₂)) = (coth ((b₁ + b₂) / 2)) * (coth ((b₁ - b₂) / 2))

proof end;

theorem Th16: :: SIN_COS8:16

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

proof end;

theorem Th17: :: SIN_COS8:17

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

proof end;

theorem Th18: :: SIN_COS8:18

for b₁, b₂ being real number holds
( ((sinh b₁) + (sinh b₂)) / ((cosh b₁) + (cosh b₂)) = tanh ((b₁ / 2) + (b₂ / 2)) & ((sinh b₁) - (sinh b₂)) / ((cosh b₁) + (cosh b₂)) = tanh ((b₁ / 2) - (b₂ / 2)) )

proof end;

theorem Th19: :: SIN_COS8:19

for b₁, b₂ being real number holds ((tanh b₁) + (tanh b₂)) / ((tanh b₁) - (tanh b₂)) = (sinh (b₁ + b₂)) / (sinh (b₁ - b₂))

proof end;

Lemma18: for b₁ being real number holds 1 + ((cosh b₁) + (cosh b₁)) <> 0

proof end;

Lemma19: for b₁ being real number holds
( (cosh b₁) + 1 > 0 & (cosh b₁) - 1 >= 0 & ((cosh b₁) + 2) + (cosh b₁) <> 0 )

proof end;

theorem Th20: :: SIN_COS8:20

for b₁, b₂ being real number holds (((sinh (b₁ - b₂)) + (sinh b₁)) + (sinh (b₁ + b₂))) / (((cosh (b₁ - b₂)) + (cosh b₁)) + (cosh (b₁ + b₂))) = tanh b₁

proof end;

Lemma20: for b₁, b₂ being real number holds
( ((sinh b₁) * (cosh b₂)) / ((cosh b₁) * (cosh b₂)) = tanh b₁ & (sinh b₁) * (cosh b₂) = (tanh b₁) * ((cosh b₁) * (cosh b₂)) & sinh b₁ = (tanh b₁) * (cosh b₁) & (sinh b₁) * (sinh b₂) = ((tanh b₁) * (tanh b₂)) * ((cosh b₁) * (cosh b₂)) )

proof end;

theorem Th21: :: SIN_COS8:21

for b₁, b₂, b₃ being real number holds
( sinh ((b₁ + b₂) + b₃) = ((((((tanh b₁) + (tanh b₂)) + (tanh b₃)) + (((tanh b₁) * (tanh b₂)) * (tanh b₃))) * (cosh b₁)) * (cosh b₂)) * (cosh b₃) & cosh ((b₁ + b₂) + b₃) = (((((1 + ((tanh b₁) * (tanh b₂))) + ((tanh b₂) * (tanh b₃))) + ((tanh b₃) * (tanh b₁))) * (cosh b₁)) * (cosh b₂)) * (cosh b₃) & tanh ((b₁ + b₂) + b₃) = ((((tanh b₁) + (tanh b₂)) + (tanh b₃)) + (((tanh b₁) * (tanh b₂)) * (tanh b₃))) / (((1 + ((tanh b₂) * (tanh b₃))) + ((tanh b₃) * (tanh b₁))) + ((tanh b₁) * (tanh b₂))) )

proof end;

theorem Th22: :: SIN_COS8:22

for b₁, b₂, b₃ being real number holds (((cosh (2 * b₁)) + (cosh (2 * b₂))) + (cosh (2 * b₃))) + (cosh (2 * ((b₁ + b₂) + b₃))) = ((4 * (cosh (b₂ + b₃))) * (cosh (b₃ + b₁))) * (cosh (b₁ + b₂))

proof end;

theorem Th23: :: SIN_COS8:23

for b₁, b₂, b₃ being real number holds (((((sinh b₁) * (sinh b₂)) * (sinh (b₂ - b₁))) + (((sinh b₂) * (sinh b₃)) * (sinh (b₃ - b₂)))) + (((sinh b₃) * (sinh b₁)) * (sinh (b₁ - b₃)))) + (((sinh (b₂ - b₁)) * (sinh (b₃ - b₂))) * (sinh (b₁ - b₃))) = 0

proof end;

theorem Th24: :: SIN_COS8:24

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

proof end;

theorem Th25: :: SIN_COS8:25

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

proof end;

theorem Th26: :: SIN_COS8:26

for b₁ being real number holds
( sinh (2 * b₁) = (2 * (sinh b₁)) * (cosh b₁) & cosh (2 * b₁) = (2 * ((cosh b₁) ^2 )) - 1 & tanh (2 * b₁) = (2 * (tanh b₁)) / (1 + ((tanh b₁) ^2 )) )

proof end;

theorem Th27: :: SIN_COS8:27

for b₁ being real number holds
( sinh (2 * b₁) = (2 * (tanh b₁)) / (1 - ((tanh b₁) ^2 )) & sinh (3 * b₁) = (sinh b₁) * ((4 * ((cosh b₁) ^2 )) - 1) & sinh (3 * b₁) = (3 * (sinh b₁)) - ((2 * (sinh b₁)) * (1 - (cosh (2 * b₁)))) & cosh (2 * b₁) = 1 + (2 * ((sinh b₁) ^2 )) & cosh (2 * b₁) = ((cosh b₁) ^2 ) + ((sinh b₁) ^2 ) & cosh (2 * b₁) = (1 + ((tanh b₁) ^2 )) / (1 - ((tanh b₁) ^2 )) & cosh (3 * b₁) = (cosh b₁) * ((4 * ((sinh b₁) ^2 )) + 1) & tanh (3 * b₁) = ((3 * (tanh b₁)) + ((tanh b₁) |^ 3)) / (1 + (3 * ((tanh b₁) ^2 ))) )

proof end;

theorem Th28: :: SIN_COS8:28

for b₁ being real number holds (((sinh (5 * b₁)) + (2 * (sinh (3 * b₁)))) + (sinh b₁)) / (((sinh (7 * b₁)) + (2 * (sinh (5 * b₁)))) + (sinh (3 * b₁))) = (sinh (3 * b₁)) / (sinh (5 * b₁))

proof end;

theorem Th29: :: SIN_COS8:29

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

proof end;

theorem Th30: :: SIN_COS8:30

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

proof end;

theorem Th31: :: SIN_COS8:31

for b₁ being real number holds
( (sinh b₁) |^ 3 = ((sinh (3 * b₁)) - (3 * (sinh b₁))) / 4 & (sinh b₁) |^ 4 = (((cosh (4 * b₁)) - (4 * (cosh (2 * b₁)))) + 3) / 8 & (sinh b₁) |^ 5 = (((sinh (5 * b₁)) - (5 * (sinh (3 * b₁)))) + (10 * (sinh b₁))) / 16 & (sinh b₁) |^ 6 = ((((cosh (6 * b₁)) - (6 * (cosh (4 * b₁)))) + (15 * (cosh (2 * b₁)))) - 10) / 32 & (sinh b₁) |^ 7 = ((((sinh (7 * b₁)) - (7 * (sinh (5 * b₁)))) + (21 * (sinh (3 * b₁)))) - (35 * (sinh b₁))) / 64 & (sinh b₁) |^ 8 = (((((cosh (8 * b₁)) - (8 * (cosh (6 * b₁)))) + (28 * (cosh (4 * b₁)))) - (56 * (cosh (2 * b₁)))) + 35) / 128 )

proof end;

theorem Th32: :: SIN_COS8:32

for b₁ being real number holds
( (cosh b₁) |^ 3 = ((cosh (3 * b₁)) + (3 * (cosh b₁))) / 4 & (cosh b₁) |^ 4 = (((cosh (4 * b₁)) + (4 * (cosh (2 * b₁)))) + 3) / 8 & (cosh b₁) |^ 5 = (((cosh (5 * b₁)) + (5 * (cosh (3 * b₁)))) + (10 * (cosh b₁))) / 16 & (cosh b₁) |^ 6 = ((((cosh (6 * b₁)) + (6 * (cosh (4 * b₁)))) + (15 * (cosh (2 * b₁)))) + 10) / 32 & (cosh b₁) |^ 7 = ((((cosh (7 * b₁)) + (7 * (cosh (5 * b₁)))) + (21 * (cosh (3 * b₁)))) + (35 * (cosh b₁))) / 64 & (cosh b₁) |^ 8 = (((((cosh (8 * b₁)) + (8 * (cosh (6 * b₁)))) + (28 * (cosh (4 * b₁)))) + (56 * (cosh (2 * b₁)))) + 35) / 128 )

proof end;

theorem Th33: :: SIN_COS8:33

for b₁, b₂ being real number holds
( (cosh (2 * b₁)) + (cos (2 * b₂)) = 2 + (2 * (((sinh b₁) ^2 ) - ((sin b₂) ^2 ))) & (cosh (2 * b₁)) - (cos (2 * b₂)) = 2 * (((sinh b₁) ^2 ) + ((sin b₂) ^2 )) )

proof end;