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


begin

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

Lm2:  for x being real number 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))) )
proofend;

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

theorem Th1: :: SIN_COS8:1
for x being real number holds
( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 )
proofend;

Lm4:  for x being real number st x <> 0 holds
( sinh x <> 0 &amp; tanh x <> 0 )
proofend;

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

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

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

Lm8:  for x being real number holds
( sinh (- x) = - (sinh x) &amp; cosh (- x) = cosh x &amp; tanh (- x) = - (tanh x) &amp; coth (- x) = - (coth x) &amp; sech (- x) = sech x &amp; cosech (- x) = - (cosech x) )
proofend;

theorem Th2: :: SIN_COS8:2
for x being real number holds
( sinh x = 1 / (cosech x) &amp; cosh x = 1 / (sech x) &amp; tanh x = 1 / (coth x) )
proofend;

Lm9:  for x being real number holds (exp_R x) + (exp_R (- x)) >= 2
proofend;

theorem Th3: :: SIN_COS8:3
for x being real number holds
( sech x <= 1 &amp; 0 < sech x &amp; sech 0 = 1 )
proofend;

theorem :: SIN_COS8:4
for x being real number st x >= 0 holds
tanh x >= 0
proofend;

theorem :: SIN_COS8:5
for x being real number holds
( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) &amp; sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) )
proofend;

theorem :: SIN_COS8:6
for x being real number
for n being Element of NAT holds
( ((cosh x) + (sinh x)) |^ n = (cosh (n * x)) + (sinh (n * x)) &amp; ((cosh x) - (sinh x)) |^ n = (cosh (n * x)) - (sinh (n * x)) )
proofend;

theorem Th7: :: SIN_COS8:7
for x being real number holds
( exp_R x = (cosh x) + (sinh x) &amp; exp_R (- x) = (cosh x) - (sinh x) &amp; exp_R x = ((cosh (x / 2)) + (sinh (x / 2))) / ((cosh (x / 2)) - (sinh (x / 2))) &amp; exp_R (- x) = ((cosh (x / 2)) - (sinh (x / 2))) / ((cosh (x / 2)) + (sinh (x / 2))) &amp; exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) &amp; exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) )
proofend;

theorem :: SIN_COS8:8
for x being real number st x <> 0 holds
( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) &amp; exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) )
proofend;

theorem :: SIN_COS8:9
for x being real number holds ((cosh x) + (sinh x)) / ((cosh x) - (sinh x)) = (1 + (tanh x)) / (1 - (tanh x))
proofend;

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

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)) &amp; (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) )
proofend;

theorem Th11: :: SIN_COS8:11
for y, z being real number holds
( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) &amp; (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) &amp; (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) &amp; (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) )
proofend;

theorem :: SIN_COS8:12
for y, z being real number holds ((sinh y) ^2) - ((cosh z) ^2) = ((sinh (y + z)) * (sinh (y - z))) - 1
proofend;

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

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) &amp; (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = 4 * ((cosh ((y - z) / 2)) ^2) )
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

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))
proofend;

theorem :: SIN_COS8:18
for y, z being real number holds
( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) &amp; ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) )
proofend;

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))
proofend;

Lm12:  for x being real number holds 1 + ((cosh x) + (cosh x)) <> 0
proofend;

Lm13:  for x being real number holds
( (cosh x) + 1 > 0 &amp; (cosh x) - 1 >= 0 &amp; ((cosh x) + 2) + (cosh x) <> 0 )
proofend;

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
proofend;

Lm14:  for y, z being real number holds
( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y &amp; (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) &amp; sinh y = (tanh y) * (cosh y) &amp; (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) )
proofend;

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) &amp; cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) &amp; 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))) )
proofend;

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))
proofend;

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
proofend;

theorem Th24: :: SIN_COS8:24
for x being real number st x >= 0 holds
sinh (x / 2) = sqrt (((cosh x) - 1) / 2)
proofend;

theorem Th25: :: SIN_COS8:25
for x being real number st x < 0 holds
sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2))
proofend;

theorem Th26: :: SIN_COS8:26
for x being real number holds
( sinh (2 * x) = (2 * (sinh x)) * (cosh x) &amp; cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 &amp; tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) )
proofend;

theorem Th27: :: SIN_COS8:27
for x being real number holds
( sinh (2 * x) = (2 * (tanh x)) / (1 - ((tanh x) ^2)) &amp; sinh (3 * x) = (sinh x) * ((4 * ((cosh x) ^2)) - 1) &amp; sinh (3 * x) = (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) &amp; cosh (2 * x) = 1 + (2 * ((sinh x) ^2)) &amp; cosh (2 * x) = ((cosh x) ^2) + ((sinh x) ^2) &amp; cosh (2 * x) = (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) &amp; cosh (3 * x) = (cosh x) * ((4 * ((sinh x) ^2)) + 1) &amp; tanh (3 * x) = ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) )
proofend;

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))
proofend;

theorem :: SIN_COS8:29
for x being real number st x >= 0 holds
tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1))
proofend;

theorem :: SIN_COS8:30
for x being real number st x < 0 holds
tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1)))
proofend;

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

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

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))) &amp; (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2) + ((sin z) ^2)) )
proofend;