let x be real number ; :: thesis: (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:6
.= (((cos x) * (cos x)) * (cos x)) * (cos x)
.= ((((cos x) |^ 1) * (cos x)) * (cos x)) * (cos x) by NEWTON:10
.= (((cos x) |^ (1 + 1)) * (cos x)) * (cos x) by NEWTON:11
.= ((cos x) |^ (2 + 1)) * (cos x) by NEWTON:11
.= (cos x) |^ (3 + 1) by NEWTON:11 ;
hence (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 ; :: thesis: verum