let x be Real; :: thesis: ( (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 )
A1: (sinh x) |^ 3 = (((4 * ((sinh x) |^ 3)) + (3 * (sinh x))) - (3 * (sinh x))) / 4
.= ((sinh (3 * x)) - (3 * (sinh x))) / 4 by SIN_COS5:43 ;
then A2: (sinh x) |^ 4 = (((sinh (3 * x)) - (3 * (sinh x))) / 4) * (sinh x) by POLYEQ_2:4
.= (((sinh (3 * x)) * (sinh x)) - (3 * ((sinh x) * (sinh x)))) / 4
.= (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) - (3 * ((sinh x) * (sinh x)))) / 4 by Th11
.= (((1 / 2) * ((cosh (4 * x)) - (cosh (2 * x)))) - (((sinh x) ^2) * 3)) / 4
.= (((1 / 2) * ((cosh (4 * x)) - (cosh (2 * x)))) - (((1 / 2) * ((cosh (2 * x)) - 1)) * 3)) / 4 by Lm7
.= (((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8 ;
A3: (sinh x) |^ 5 = (sinh x) |^ (4 + 1)
.= ((((cosh (4 * x)) - (4 * (cosh (2 * x)))) + 3) / 8) * (sinh x) by
.= ((((cosh (4 * x)) * (sinh x)) - (4 * ((cosh (2 * x)) * (sinh x)))) + (3 * (sinh x))) / 8
.= ((((1 / 2) * ((sinh ((4 * x) + (1 * x))) - (sinh ((4 * x) - (1 * x))))) - (4 * ((cosh (2 * x)) * (sinh x)))) + (3 * (sinh x))) / 8 by Th11
.= ((((1 / 2) * ((sinh (5 * x)) - (sinh (3 * x)))) - (4 * ((1 / 2) * ((sinh ((2 * x) + (1 * x))) - (sinh ((2 * x) - (1 * x))))))) + (3 * (sinh x))) / 8 by Th11
.= (((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16 ;
A4: (sinh x) |^ 6 = (sinh x) |^ (5 + 1)
.= ((((sinh (5 * x)) - (5 * (sinh (3 * x)))) + (10 * (sinh x))) / 16) * (sinh x) by
.= ((((sinh (5 * x)) * (sinh x)) - (5 * ((sinh (3 * x)) * (sinh x)))) + (10 * ((sinh x) * (sinh x)))) / 16
.= ((((1 / 2) * ((cosh ((5 * x) + (1 * x))) - (cosh ((5 * x) - (1 * x))))) - (5 * ((sinh (3 * x)) * (sinh x)))) + (10 * ((sinh x) * (sinh x)))) / 16 by Th11
.= ((((1 / 2) * ((cosh (6 * x)) - (cosh (4 * x)))) - (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) * 5)) + (10 * ((sinh x) * (sinh x)))) / 16 by Th11
.= (((1 / 2) * (((cosh (6 * x)) - (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (10 * ((sinh x) ^2))) / 16
.= (((1 / 2) * (((cosh (6 * x)) - (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (((1 / 2) * ((cosh (2 * x)) - 1)) * 10)) / 16 by Lm7
.= ((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32 ;
A5: (sinh x) |^ 7 = (sinh x) |^ (6 + 1)
.= (((((cosh (6 * x)) - (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) - 10) / 32) * (sinh x) by
.= (((((cosh (6 * x)) * (sinh x)) - ((6 * (cosh (4 * x))) * (sinh x))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32
.= (((((1 / 2) * ((sinh ((6 * x) + (1 * x))) - (sinh ((6 * x) - (1 * x))))) - ((6 * (cosh (4 * x))) * (sinh x))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 by Th11
.= (((((1 / 2) * ((sinh (7 * x)) - (sinh (5 * x)))) - (6 * ((cosh (4 * x)) * (sinh x)))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32
.= (((((1 / 2) * ((sinh (7 * x)) - (sinh (5 * x)))) - (6 * ((1 / 2) * ((sinh ((4 * x) + (1 * x))) - (sinh ((4 * x) - (1 * x))))))) + ((15 * (cosh (2 * x))) * (sinh x))) - (10 * (sinh x))) / 32 by Th11
.= ((((1 / 2) * (((sinh (7 * x)) - (7 * (sinh (5 * x)))) + ((sinh (3 * x)) * 6))) + (15 * ((cosh (2 * x)) * (sinh x)))) - (10 * (sinh x))) / 32
.= ((((1 / 2) * (((sinh (7 * x)) - (7 * (sinh (5 * x)))) + ((sinh (3 * x)) * 6))) + (15 * ((1 / 2) * ((sinh ((2 * x) + (1 * x))) - (sinh ((2 * x) - (1 * x))))))) - (10 * (sinh x))) / 32 by Th11
.= ((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64 ;
(sinh x) |^ 8 = (sinh x) |^ (7 + 1)
.= (((((sinh (7 * x)) - (7 * (sinh (5 * x)))) + (21 * (sinh (3 * x)))) - (35 * (sinh x))) / 64) * (sinh x) by
.= (((((sinh (7 * x)) * (sinh x)) - (7 * ((sinh (5 * x)) * (sinh x)))) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64
.= (((((1 / 2) * ((cosh ((7 * x) + (1 * x))) - (cosh ((7 * x) - (1 * x))))) - (7 * ((sinh (5 * x)) * (sinh x)))) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11
.= (((((1 / 2) * ((cosh (8 * x)) - (cosh (6 * x)))) - (((1 / 2) * ((cosh ((5 * x) + (1 * x))) - (cosh ((5 * x) - (1 * x))))) * 7)) + (21 * ((sinh (3 * x)) * (sinh x)))) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11
.= ((((1 / 2) * (((cosh (8 * x)) - (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (((1 / 2) * ((cosh ((3 * x) + (1 * x))) - (cosh ((3 * x) - (1 * x))))) * 21)) - (35 * ((sinh x) * (sinh x)))) / 64 by Th11
.= (((1 / 2) * ((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (- ((cosh (2 * x)) * 21)))) - (35 * ((sinh x) ^2))) / 64
.= (((1 / 2) * ((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) + (- ((cosh (2 * x)) * 21)))) - (((1 / 2) * ((cosh (2 * x)) - 1)) * 35)) / 64 by Lm7
.= (((((cosh (8 * x)) - (8 * (cosh (6 * x)))) + (28 * (cosh (4 * x)))) - (56 * (cosh (2 * x)))) + 35) / 128 ;
hence ( (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 ) by A1, A2, A3, A4, A5; :: thesis: verum