let x be Real; :: thesis:
A1: (cosh x) |^ 3 = (cosh x) |^ ((1 + 1) + 1)
.= ((cosh x) |^ (1 + 1)) * (cosh x) by NEWTON:6
.= (((cosh x) |^ 1) * (cosh x)) * (cosh x) by NEWTON:6
.= ((((cosh x) ^2) * (cosh x)) + (3 * ((cosh x) * ((((cosh x) ^2) - ((sinh x) ^2)) + ((sinh x) ^2))))) / 4
.= ((((cosh x) ^2) * (cosh x)) + (3 * ((cosh x) * (1 + ((sinh x) ^2))))) / 4 by Lm3
.= ((((cosh x) * (((cosh x) * (cosh x)) + ((sinh x) ^2))) + (2 * ((cosh x) * ((sinh x) ^2)))) + (3 * (cosh x))) / 4
.= ((((cosh x) * (cosh (x + x))) + (2 * ((cosh x) * ((sinh x) ^2)))) + (3 * (cosh x))) / 4 by Lm10
.= ((((cosh x) * (cosh (2 * x))) + (((2 * (sinh x)) * (cosh x)) * (sinh x))) + (3 * (cosh x))) / 4
.= ((((cosh (2 * x)) * (cosh x)) + ((sinh (2 * x)) * (sinh x))) + (3 * (cosh x))) / 4 by Th26
.= ((cosh ((x + x) + x)) + (3 * (cosh x))) / 4 by Lm10
.= ((cosh (3 * x)) + (3 * (cosh x))) / 4 ;
then A2: (cosh x) |^ 4 = (((cosh (3 * x)) + (3 * (cosh x))) / 4) * (cosh x) by POLYEQ_2:4
.= (((cosh (3 * x)) * (cosh x)) + (3 * ((cosh x) * (cosh x)))) / 4
.= (((1 / 2) * ((cosh ((3 * x) + (1 * x))) + (cosh ((3 * x) - x)))) + (3 * ((cosh x) * (cosh x)))) / 4 by Th11
.= (((1 / 2) * ((cosh (4 * x)) + (cosh (2 * x)))) + (3 * ((1 / 2) * ((cosh (x + x)) + (cosh (x - x)))))) / 4 by Th11
.= (((1 / 2) * ((cosh (4 * x)) + (cosh (2 * x)))) + (((1 / 2) * ((cosh (2 * x)) + 1)) * 3)) / 4 by SIN_COS2:15, SIN_COS2:def 4
.= (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 ;
A3: (cosh x) |^ 5 = (cosh x) |^ (4 + 1)
.= ((((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8) * (cosh x) by A2, NEWTON:6
.= ((((cosh (4 * x)) * (cosh x)) + (4 * ((cosh (2 * x)) * (cosh x)))) + (3 * (cosh x))) / 8
.= ((((1 / 2) * ((cosh ((4 * x) + (1 * x))) + (cosh ((4 * x) - x)))) + (4 * ((cosh (2 * x)) * (cosh x)))) + (3 * (cosh x))) / 8 by Th11
.= ((((1 / 2) * ((cosh (5 * x)) + (cosh (3 * x)))) + (4 * ((1 / 2) * ((cosh ((2 * x) + (1 * x))) + (cosh ((2 * x) - x)))))) + (3 * (cosh x))) / 8 by Th11
.= (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 ;
A4: (cosh x) |^ 6 = (cosh x) |^ (5 + 1)
.= ((((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16) * (cosh x) by A3, NEWTON:6
.= ((((cosh (5 * x)) * (cosh x)) + (5 * ((cosh (3 * x)) * (cosh x)))) + (10 * ((cosh x) * (cosh x)))) / 16
.= ((((1 / 2) * ((cosh ((5 * x) + x)) + (cosh ((5 * x) - x)))) + (5 * ((cosh (3 * x)) * (cosh x)))) + (10 * ((cosh x) * (cosh x)))) / 16 by Th11
.= ((((1 / 2) * ((cosh ((5 * x) + x)) + (cosh ((5 * x) - x)))) + (((1 / 2) * ((cosh ((3 * x) + x)) + (cosh ((3 * x) - x)))) * 5)) + (10 * ((cosh x) * (cosh x)))) / 16 by Th11
.= (((1 / 2) * (((cosh (6 * x)) + (6 * (cosh (4 * x)))) + ((cosh (2 * x)) * 5))) + (10 * ((cosh 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: (cosh x) |^ 7 = (cosh x) |^ (6 + 1)
.= (((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32) * (cosh x) by A4, NEWTON:6
.= (((((cosh (6 * x)) * (cosh x)) + (6 * ((cosh (4 * x)) * (cosh x)))) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32
.= (((((1 / 2) * ((cosh ((6 * x) + (1 * x))) + (cosh ((6 * x) - (1 * x))))) + (6 * ((cosh (4 * x)) * (cosh x)))) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32 by Th11
.= (((((1 / 2) * ((cosh (7 * x)) + (cosh (5 * x)))) + (((1 / 2) * ((cosh ((4 * x) + x)) + (cosh ((4 * x) - x)))) * 6)) + (15 * ((cosh (2 * x)) * (cosh x)))) + (10 * (cosh x))) / 32 by Th11
.= ((((1 / 2) * (((cosh (7 * x)) + (7 * (cosh (5 * x)))) + ((cosh (3 * x)) * 6))) + (((1 / 2) * ((cosh ((2 * x) + x)) + (cosh ((2 * x) - x)))) * 15)) + (10 * (cosh x))) / 32 by Th11
.= ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 ;
(cosh x) |^ 8 = (cosh x) |^ (7 + 1)
.= (((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64) * (cosh x) by A5, NEWTON:6
.= (((((cosh (7 * x)) * (cosh x)) + ((7 * (cosh (5 * x))) * (cosh x))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64
.= (((((1 / 2) * ((cosh ((7 * x) + (1 * x))) + (cosh ((7 * x) - x)))) + ((7 * (cosh (5 * x))) * (cosh x))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 by Th11
.= (((((1 / 2) * ((cosh (8 * x)) + (cosh (6 * x)))) + (7 * ((cosh (5 * x)) * (cosh x)))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64
.= (((((1 / 2) * ((cosh (8 * x)) + (cosh (6 * x)))) + (7 * ((1 / 2) * ((cosh ((5 * x) + (1 * x))) + (cosh ((5 * x) - (1 * x))))))) + ((21 * (cosh (3 * x))) * (cosh x))) + (35 * ((cosh x) ^2))) / 64 by Th11
.= ((((1 / 2) * (((cosh (8 * x)) + (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (21 * ((cosh (3 * x)) * (cosh x)))) + (35 * ((cosh x) ^2))) / 64
.= ((((1 / 2) * (((cosh (8 * x)) + (8 * (cosh (6 * x)))) + ((cosh (4 * x)) * 7))) + (21 * ((1 / 2) * ((cosh ((3 * x) + (1 * x))) + (cosh ((3 * x) - x)))))) + (35 * ((cosh x) ^2))) / 64 by Th11
.= (((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 ( (cosh x) |^ 3 = ((cosh (3 * x)) + (3 * (cosh x))) / 4 & (cosh x) |^ 4 = (((cosh (4 * x)) + (4 * (cosh (2 * x)))) + 3) / 8 & (cosh x) |^ 5 = (((cosh (5 * x)) + (5 * (cosh (3 * x)))) + (10 * (cosh x))) / 16 & (cosh x) |^ 6 = ((((cosh (6 * x)) + (6 * (cosh (4 * x)))) + (15 * (cosh (2 * x)))) + 10) / 32 & (cosh x) |^ 7 = ((((cosh (7 * x)) + (7 * (cosh (5 * x)))) + (21 * (cosh (3 * x)))) + (35 * (cosh x))) / 64 & (cosh 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: