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