:: Formulas and Identities of Hyperbolic Functions
:: by Pacharapokin Chanapat and Hiroshi Yamazaki
::
:: Received November 7, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


Lm1: for x being Real holds
( cosh x >= 1 & cosh 0 = 1 & sinh 0 = 0 )
proof end;

Lm2: for x being Real holds
( sinh x = ((exp_R x) - (exp_R (- x))) / 2 & cosh x = ((exp_R x) + (exp_R (- x))) / 2 & tanh x = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) )
proof end;

Lm3: for x being Real 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 holds
( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 )
proof end;

Lm4: for x being Real st x <> 0 holds
( sinh x <> 0 & tanh x <> 0 )
proof end;

Lm5: for y, z being Real st y - z <> 0 holds
sinh ((y / 2) - (z / 2)) <> 0
proof end;

Lm6: for y, z being Real st y + z <> 0 holds
sinh ((y / 2) + (z / 2)) <> 0
proof end;

Lm7: for x being Real holds
( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) )
proof end;

Lm8: for x being Real 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 holds
( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) )
proof end;

Lm9: for x being Real holds (exp_R x) + (exp_R (- x)) >= 2
proof end;

theorem Th3: :: SIN_COS8:3
for x being Real holds
( sech x <= 1 & 0 < sech x & sech 0 = 1 )
proof end;

theorem :: SIN_COS8:4
for x being Real st x >= 0 holds
tanh x >= 0
proof end;

theorem :: SIN_COS8:5
for x being Real 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
for n being Element of 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 holds
( exp_R x = (cosh x) + (sinh x) & exp_R (- x) = (cosh x) - (sinh x) & exp_R x = ((cosh (x / 2)) + (sinh (x / 2))) / ((cosh (x / 2)) - (sinh (x / 2))) & exp_R (- x) = ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (sinh (x / 2))) & exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) & exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) )
proof end;

theorem :: SIN_COS8:8
for x being Real st x <> 0 holds
( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) )
proof end;

theorem :: SIN_COS8:9
for x being Real holds ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x))
proof end;

Lm10: for y, z being Real 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 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 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 holds ((sinh y) ^2) - ((cosh z) ^2) = ((sinh (y + z)) * (sinh (y - z))) - 1
proof end;

Lm11: for y, z being Real 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 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 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 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 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 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 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 holds ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z))
proof end;

Lm12: for x being Real holds 1 + ((cosh x) + (cosh x)) <> 0
proof end;

Lm13: for x being Real 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 holds (((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) = tanh y
proof end;

Lm14: for y, z being Real 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 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 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 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 st x >= 0 holds
sinh (x / 2) = sqrt (((cosh x) - 1) / 2)
proof end;

theorem Th25: :: SIN_COS8:25
for x being Real st x < 0 holds
sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2))
proof end;

theorem Th26: :: SIN_COS8:26
for x being Real 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 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 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 st x >= 0 holds
tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1))
proof end;

theorem :: SIN_COS8:30
for x being Real st x < 0 holds
tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1)))
proof end;

theorem :: SIN_COS8:31
for x being Real 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 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 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;