let x be Real; :: 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:75 ;
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:29
.= - ((- 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