:: SIN_COS8 semantic presentation

Lm1: for x being real number holds
( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 )

proof end;

Lm2: for x being real number st x >= 0 holds
sinh x >= 0
by SIN_COS5:46;

Lm3: for x being real number holds
( sinh x = ((exp x) - (exp (- x))) / 2 & cosh x = ((exp x) + (exp (- x))) / 2 & tanh x = ((exp x) - (exp (- x))) / ((exp x) + (exp (- x))) )

proof end;

Lm4: for x being real number holds
( ((cosh x) ^2 ) - ((sinh x) ^2 ) = 1 & ((cosh x) * (cosh x)) - ((sinh x) * (sinh x)) = 1 )

proof end;

theorem Th1: :: SIN_COS8:1

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

proof end;

Lm5: for x being real number st x <> 0 holds
( sinh x <> 0 & tanh x <> 0 )

proof end;

Lm6: for y, z being real number st y - z <> 0 holds
sinh ((y / 2) - (z / 2)) <> 0

proof end;

Lm7: for y, z being real number st y + z <> 0 holds
sinh ((y / 2) + (z / 2)) <> 0

proof end;

Lm8: for x being real number holds
( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) )

proof end;

Lm9: for x being real number holds
( sinh (- x) = - (sinh x) & cosh (- x) = cosh x & tanh (- x) = - (tanh x) & coth (- x) = - (coth x) & sech (- x) = sech x & cosech (- x) = - (cosech x) )

proof end;

theorem Th2: :: SIN_COS8:2

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

proof end;

Lm10: for x being real number holds (exp x) + (exp (- x)) >= 2

proof end;

theorem Th3: :: SIN_COS8:3

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

proof end;

theorem :: SIN_COS8:4

for x being real number st x >= 0 holds
tanh x >= 0

proof end;

theorem :: SIN_COS8:5

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

proof end;

theorem :: SIN_COS8:6

for x being real number
for n being Nat holds
( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) & ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) )

proof end;

theorem Th7: :: SIN_COS8:7

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

proof end;

theorem :: SIN_COS8:8

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

proof end;

theorem :: SIN_COS8:9

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

proof end;

Lm11: for y, z being real number holds
( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) )

proof end;

theorem :: SIN_COS8:10

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

proof end;

theorem Th11: :: SIN_COS8:11

for y, z being real number holds
( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) )

proof end;

theorem :: SIN_COS8:12

for y, z being real number holds ((sinh y) ^2 ) - ((cosh z) ^2 ) = ((sinh (y + z)) * (sinh (y - z))) - 1

proof end;

Lm12: for y, z being real number holds
( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) )

proof end;

theorem :: SIN_COS8:13

for y, z being real number holds
( (((sinh y) - (sinh z)) ^2 ) - (((cosh y) - (cosh z)) ^2 ) = 4 * ((sinh ((y - z) / 2)) ^2 ) & (((cosh y) + (cosh z)) ^2 ) - (((sinh y) + (sinh z)) ^2 ) = 4 * ((cosh ((y - z) / 2)) ^2 ) )

proof end;

theorem :: SIN_COS8:14

for y, z being real number holds ((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) = (tanh ((y + z) / 2)) * (coth ((y - z) / 2))

proof end;

theorem :: SIN_COS8:15

for y, z being real number holds ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2))

proof end;

theorem :: SIN_COS8:16

for y, z being real number st y - z <> 0 holds
((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z))

proof end;

theorem :: SIN_COS8:17

for y, z being real number st y + z <> 0 holds
((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) + (sinh z))

proof end;

theorem :: SIN_COS8:18

for y, z being real number holds
( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) )

proof end;

theorem :: SIN_COS8:19

for y, z being real number holds ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z))

proof end;

Lm13: for x being real number holds 1 + ((cosh x) + (cosh x)) <> 0

proof end;

Lm14: for x being real number holds
( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 & ((cosh x) + 2) + (cosh x) <> 0 )

proof end;

theorem :: SIN_COS8:20

for y, z being real number holds (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = tanh y

proof end;

Lm15: for y, z being real number holds
( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) )

proof end;

theorem Th21: :: SIN_COS8:21

for y, z, w being real number holds
( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) )

proof end;

theorem :: SIN_COS8:22

for y, z, w being real number holds (((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) = ((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z))

proof end;

theorem :: SIN_COS8:23

for y, z, w being real number holds (((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) = 0

proof end;

theorem Th24: :: SIN_COS8:24

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

proof end;

theorem Th25: :: SIN_COS8:25

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

proof end;

theorem Th26: :: SIN_COS8:26

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

proof end;

theorem Th27: :: SIN_COS8:27

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

proof end;

theorem :: SIN_COS8:28

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

proof end;

theorem :: SIN_COS8:29

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

proof end;

theorem :: SIN_COS8:30

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

proof end;

theorem :: SIN_COS8:31

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

proof end;

theorem :: SIN_COS8:32

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

proof end;

theorem :: SIN_COS8:33

for y, z being real number holds
( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2 ) - ((sin z) ^2 ))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2 ) + ((sin z) ^2 )) )

proof end;