let x be real number ; :: 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 A1, XCMPLX_1:89
.= (((2 * (sinh x)) * (cosh x)) * (cosh x)) / (cosh x) by XCMPLX_1:75
.= ((2 * (sinh x)) * ((cosh x) * (cosh x))) / (cosh x)
.= ((2 * (sinh x)) / (cosh x)) * ((cosh x) * (cosh x)) by XCMPLX_1:75
.= (2 * ((sinh x) / (cosh x))) * ((cosh x) * (cosh x)) by XCMPLX_1:75
.= (2 * (tanh x)) * ((cosh x) * (cosh x)) by Th1
.= (2 * (tanh x)) / (1 / ((cosh x) * (cosh x))) by XCMPLX_1:101
.= (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:121
.= (2 * (tanh x)) / ((((cosh x) / (cosh x)) * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by XCMPLX_1:77
.= (2 * (tanh x)) / ((1 * ((cosh x) / (cosh x))) - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by A1, XCMPLX_1:60
.= (2 * (tanh x)) / (1 - (((sinh x) * (sinh x)) / ((cosh x) * (cosh x)))) by A1, XCMPLX_1:60
.= (2 * (tanh x)) / (1 - (((sinh x) / (cosh x)) * ((sinh x) / (cosh x)))) by XCMPLX_1:77
.= (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:11
.= ((4 * ((cosh x) |^ (1 + 1))) - 3) * (cosh x)
.= ((4 * (((cosh x) |^ 1) * (cosh x))) - 3) * (cosh x) by NEWTON:11
.= ((4 * ((((cosh x) ^2 ) - ((sinh x) ^2 )) + ((sinh x) ^2 ))) - 3) * (cosh x) by NEWTON:10
.= ((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))) by NEWTON:10
.= ((3 * (tanh x)) + (((tanh x) |^ (1 + 1)) * (tanh x))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:11
.= ((3 * (tanh x)) + ((tanh x) |^ ((1 + 1) + 1))) / (((1 + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) + ((tanh x) * (tanh x))) by NEWTON:11
.= ((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:77
.= (1 / ((sech x) ^2 )) + ((((sinh x) ^2 ) / ((cosh x) ^2 )) * ((cosh x) ^2 )) by A6, XCMPLX_1:6, XCMPLX_1:88
.= (1 / ((sech x) ^2 )) + ((((sinh x) / (cosh x)) ^2 ) * ((cosh x) ^2 )) by XCMPLX_1:77
.= (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:101
.= (1 / ((sech x) ^2 )) + (((tanh x) ^2 ) / ((1 / (cosh x)) ^2 )) by XCMPLX_1:77
.= (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:63
.= (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:11
.= (sinh x) * ((4 * ((sinh x) |^ (1 + 1))) + 3)
.= (sinh x) * ((4 * (((sinh x) |^ 1) * (sinh x))) + 3) by NEWTON:11
.= (sinh x) * ((4 * (((cosh x) ^2 ) - (((cosh x) ^2 ) - ((sinh x) ^2 )))) + 3) by NEWTON:10
.= (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