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