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