let x be real number ; :: thesis: ( cos (2 * x) = ((cos x) ^2 ) - ((sin x) ^2 ) & cos (2 * x) = (2 * ((cos x) ^2 )) - 1 & cos (2 * x) = 1 - (2 * ((sin x) ^2 )) )
A1: cos (2 * x) = cos (x + x)
.= ((cos x) ^2 ) - ((sin x) ^2 ) by SIN_COS:80 ;
then cos (2 * x) = ((((cos x) ^2 ) - ((sin x) ^2 )) - 1) + 1
.= ((((cos x) ^2 ) - ((sin x) ^2 )) - (((cos x) ^2 ) + ((sin x) ^2 ))) + 1 by SIN_COS:32
.= - ((- 1) + (2 * ((sin x) ^2 ))) ;
hence ( cos (2 * x) = ((cos x) ^2 ) - ((sin x) ^2 ) & cos (2 * x) = (2 * ((cos x) ^2 )) - 1 & cos (2 * x) = 1 - (2 * ((sin x) ^2 )) ) by A1; :: thesis: verum