let x be Real; sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
sin (3 * x) =
sin ((x + x) + x)
.=
((sin (2 * x)) * (cos x)) + ((cos (x + x)) * (sin x))
by SIN_COS:75
.=
(((2 * (sin x)) * (cos x)) * (cos x)) + ((cos (2 * x)) * (sin x))
by Th5
.=
((2 * (sin x)) * ((cos x) * (cos x))) + ((1 - (2 * ((sin x) ^2))) * (sin x))
by Th7
.=
((2 * (sin x)) * (1 - ((sin x) ^2))) + ((1 - (2 * ((sin x) ^2))) * (sin x))
by SIN_COS4:5
.=
(((2 * (sin x)) * 1) - ((2 * (sin x)) * ((sin x) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
.=
(((2 * (sin x)) * 1) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
.=
(((2 * (sin x)) * 1) - ((2 * ((sin x) |^ (1 + 1))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
by NEWTON:6
.=
(((2 * (sin x)) * 1) - (2 * (((sin x) |^ 2) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
.=
(((2 * (sin x)) * 1) - (2 * ((sin x) |^ (2 + 1)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
by NEWTON:6
.=
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x)))
.=
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * ((sin x) |^ (1 + 1))) * (sin x)))
by NEWTON:6
.=
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * (((sin x) |^ (1 + 1)) * (sin x))))
.=
((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * ((sin x) |^ (2 + 1))))
by NEWTON:6
.=
- ((- (3 * (sin x))) + (4 * ((sin x) |^ 3)))
;
hence
sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
; verum