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