let x be Real; :: thesis: ( 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))) )
A1: cosh x <> 0 by Lm1;
A2: sinh (2 * x) = (2 * (sinh x)) * (cosh x) by Th26
.= ((2 * (sinh x)) * (cosh x)) * ((cosh x) / (cosh x)) by
.= (((2 * (sinh x)) * (cosh x)) * (cosh x)) / (cosh x) by XCMPLX_1:74
.= ((2 * (sinh x)) * ((cosh x) * (cosh x))) / (cosh x)
.= ((2 * (sinh x)) / (cosh x)) * ((cosh x) * (cosh x)) by XCMPLX_1:74
.= (2 * ((sinh x) / (cosh x))) * ((cosh x) * (cosh x)) by XCMPLX_1:74
.= (2 * (tanh x)) * ((cosh x) * (cosh x)) by Th1
.= (2 * (tanh x)) / (1 / ((cosh x) * (cosh x))) by XCMPLX_1:100
.= (2 * (tanh x)) / ((((cosh x) * (cosh x)) - ((sinh x) ^2)) / ((cosh x) * (cosh x))) by Lm3
.= (2 * (tanh x)) / ((((cosh x) * (cosh x)) / ((cosh x) * (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by XCMPLX_1:120
.= (2 * (tanh x)) / ((((cosh x) / (cosh x)) * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by XCMPLX_1:76
.= (2 * (tanh x)) / ((1 * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by
.= (2 * (tanh x)) / (1 - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by
.= (2 * (tanh x)) / (1 - (((sinh x) / (cosh x)) * ((sinh x) / (cosh x)))) by XCMPLX_1:76
.= (2 * (tanh x)) / (1 - ((tanh x) * ((sinh x) / (cosh x)))) by Th1
.= (2 * (tanh x)) / (1 - ((tanh x) ^2)) by Th1 ;
A3: cosh (3 * x) = (4 * ((cosh x) |^ (2 + 1))) - (3 * (cosh x)) by SIN_COS5:44
.= (4 * (((cosh x) |^ 2) * (cosh x))) - (3 * (cosh x)) by NEWTON:6
.= ((4 * ((cosh x) |^ (1 + 1))) - 3) * (cosh x)
.= ((4 * (((cosh x) |^ 1) * (cosh x))) - 3) * (cosh x) by NEWTON:6
.= ((4 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))) - 3) * (cosh x)
.= ((4 * (1 + ((sinh x) ^2))) - 3) * (cosh x) by Lm3
.= (cosh x) * ((4 * ((sinh x) ^2)) + 1) ;
A4: cosh (2 * x) = (2 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))) - 1 by Th26
.= (2 * (1 + ((sinh x) ^2))) - 1 by Lm3
.= 1 + (2 * ((sinh x) ^2)) ;
A5: tanh (3 * x) = tanh ((x + x) + x)
.= ((((tanh x) + (tanh x)) + (tanh x)) + (((tanh x) * (tanh x)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by Th21
.= ((3 * (tanh x)) + ((((tanh x) |^ 1) * (tanh x)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x)))
.= ((3 * (tanh x)) + (((tanh x) |^ (1 + 1)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:6
.= ((3 * (tanh x)) + ((tanh x) |^ ((1 + 1) + 1))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:6
.= ((3 * (tanh x)) + ((tanh x) |^ 3)) / (1 + (3 * ((tanh x) ^2))) ;
A6: cosh x <> 0 by Lm1;
A7: cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 by Th26
.= (2 * ((cosh x) ^2)) - (((cosh x) ^2) - ((sinh x) ^2)) by Lm3
.= ((cosh x) ^2) + ((sinh x) ^2) ;
then A8: cosh (2 * x) = ((1 / (sech x)) ^2) + ((sinh x) ^2) by Th2
.= (1 / ((sech x) ^2)) + (((sinh x) ^2) * (1 ^2)) by XCMPLX_1:76
.= (1 / ((sech x) ^2)) + ((((sinh x) ^2) / ((cosh x) ^2)) * ((cosh x) ^2)) by
.= (1 / ((sech x) ^2)) + ((((sinh x) / (cosh x)) ^2) * ((cosh x) ^2)) by XCMPLX_1:76
.= (1 / ((sech x) ^2)) + (((tanh x) ^2) * ((cosh x) ^2)) by Th1
.= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((1 ^2) / ((cosh x) ^2))) by XCMPLX_1:100
.= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((1 / (cosh x)) ^2)) by XCMPLX_1:76
.= (1 / ((sech x) ^2)) + (((tanh x) ^2) / ((sech x) ^2)) by SIN_COS5:def 2
.= (1 + ((tanh x) ^2)) / ((((sech x) ^2) + ((tanh x) ^2)) - ((tanh x) ^2)) by XCMPLX_1:62
.= (1 + ((tanh x) ^2)) / (1 - ((tanh x) ^2)) by SIN_COS5:38 ;
A9: sinh (3 * x) = (4 * ((sinh x) |^ (2 + 1))) + (3 * (sinh x)) by SIN_COS5:43
.= (4 * (((sinh x) |^ 2) * (sinh x))) + (3 * (sinh x)) by NEWTON:6
.= (sinh x) * ((4 * ((sinh x) |^ (1 + 1))) + 3)
.= (sinh x) * ((4 * (((sinh x) |^ 1) * (sinh x))) + 3) by NEWTON:6
.= (sinh x) * ((4 * (((cosh x) ^2) - (((cosh x) ^2) - ((sinh x) ^2)))) + 3)
.= (sinh x) * ((4 * (((cosh x) ^2) - 1)) + 3) by Lm3
.= (sinh x) * ((4 * ((cosh x) ^2)) - 1) ;
then sinh (3 * x) = ((sinh x) * (4 * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2)))) - (sinh x)
.= ((sinh x) * (4 * (1 + ((sinh x) ^2)))) - (sinh x) by Lm3
.= ((4 * (sinh x)) + ((sinh x) * ((2 * (((cosh x) ^2) - (((cosh x) ^2) - ((sinh x) ^2)))) + (2 * ((sinh x) ^2))))) - (sinh x)
.= ((4 * (sinh x)) + ((sinh x) * ((2 * (((cosh x) ^2) - 1)) + (2 * ((sinh x) ^2))))) - (sinh x) by Lm3
.= ((4 * (sinh x)) + ((sinh x) * (2 * ((((cosh x) * (cosh x)) + ((sinh x) ^2)) - 1)))) - (sinh x)
.= ((4 * (sinh x)) + ((sinh x) * (2 * ((cosh (x + x)) - 1)))) - (sinh x) by Lm10
.= (3 * (sinh x)) - ((2 * (sinh x)) * (1 - (cosh (2 * x)))) ;
hence ( 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))) ) by A2, A9, A4, A7, A8, A3, A5; :: thesis: verum