let x be Real; cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5))
set t = cosh . x;
set u = sinh . x;
cosh (5 * x) =
cosh . ((4 * x) + x)
by SIN_COS2:def 4
.=
((cosh . (2 * (2 * x))) * (cosh . x)) + ((sinh . (4 * x)) * (sinh . x))
by SIN_COS2:20
.=
((1 + (2 * ((sinh . (2 * x)) ^2))) * (cosh . x)) + ((sinh . (4 * x)) * (sinh . x))
by Th69
.=
((1 + (2 * (((2 * (sinh . x)) * (cosh . x)) ^2))) * (cosh . x)) + ((sinh . (2 * (2 * x))) * (sinh . x))
by SIN_COS2:23
.=
((cosh . x) + ((8 * ((sinh . x) ^2)) * (((cosh . x) ^2) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x))
.=
((cosh . x) + ((8 * ((sinh . x) ^2)) * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x))
.=
((cosh . x) + ((8 * ((sinh . x) ^2)) * (((cosh . x) |^ (1 + 1)) * (cosh . x)))) + ((sinh . (2 * (2 * x))) * (sinh . x))
by NEWTON:6
.=
((cosh . x) + ((8 * ((sinh . x) ^2)) * ((cosh . x) |^ (2 + 1)))) + ((sinh . (2 * (2 * x))) * (sinh . x))
by NEWTON:6
.=
((cosh . x) + ((8 * (((cosh . x) ^2) - 1)) * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x))
by Th71
.=
(((cosh . x) + (8 * ((((cosh . x) |^ 3) * (cosh . x)) * (cosh . x)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x))
.=
(((cosh . x) + (8 * (((cosh . x) |^ (3 + 1)) * (cosh . x)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x))
by NEWTON:6
.=
(((cosh . x) + (8 * ((cosh . x) |^ (4 + 1)))) - (8 * ((cosh . x) |^ 3))) + ((sinh . (2 * (2 * x))) * (sinh . x))
by NEWTON:6
.=
(((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((2 * (sinh . (2 * x))) * (cosh . (2 * x))) * (sinh . x))
by SIN_COS2:23
.=
(((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((2 * ((2 * (sinh . x)) * (cosh . x))) * (cosh . (2 * x))) * (sinh . x))
by SIN_COS2:23
.=
(((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((4 * ((sinh . x) ^2)) * (cosh . x)) * (cosh . (2 * x)))
.=
(((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (((4 * (((cosh . x) ^2) - 1)) * (cosh . x)) * (cosh . (2 * x)))
by Th71
.=
((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * (((cosh . x) * (cosh . x)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
.=
((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
.=
((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
by NEWTON:6
.=
((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((cosh . x) |^ (2 + 1))) * (cosh . (2 * x)))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
by NEWTON:6
.=
((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + ((4 * ((cosh . x) |^ 3)) * ((2 * ((cosh . x) ^2)) - 1))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
by SIN_COS2:23
.=
(((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * ((((cosh . x) |^ 3) * (cosh . x)) * (cosh . x)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
.=
(((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * (((cosh . x) |^ (3 + 1)) * (cosh . x)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
by NEWTON:6
.=
(((((cosh . x) + (8 * ((cosh . x) |^ 5))) - (8 * ((cosh . x) |^ 3))) + (8 * ((cosh . x) |^ (4 + 1)))) - (4 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * (cosh . (2 * x)))
by NEWTON:6
.=
(((cosh . x) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - ((4 * (cosh . x)) * ((2 * ((cosh . x) ^2)) - 1))
by SIN_COS2:23
.=
(((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * (((cosh . x) * (cosh . x)) * (cosh . x)))
.=
(((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x)))
.=
(((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * (((cosh . x) |^ (1 + 1)) * (cosh . x)))
by NEWTON:6
.=
(((5 * (cosh . x)) + (16 * ((cosh . x) |^ 5))) - (12 * ((cosh . x) |^ 3))) - (8 * ((cosh . x) |^ (2 + 1)))
by NEWTON:6
.=
((5 * (cosh . x)) - (20 * ((cosh . x) |^ 3))) + (16 * ((cosh . x) |^ 5))
.=
((5 * (cosh x)) - (20 * ((cosh . x) |^ 3))) + (16 * ((cosh . x) |^ 5))
by SIN_COS2:def 4
.=
((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh . x) |^ 5))
by SIN_COS2:def 4
.=
((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5))
by SIN_COS2:def 4
;
hence
cosh (5 * x) = ((5 * (cosh x)) - (20 * ((cosh x) |^ 3))) + (16 * ((cosh x) |^ 5))
; verum