let x be Real; :: thesis: sin (2 * x) = (2 * (sin x)) * (cos x)
sin (2 * x) = sin (x + x)
.= ((sin x) * (cos x)) + ((cos x) * (sin x)) by SIN_COS:75
.= (2 * (sin x)) * (cos x) ;
hence sin (2 * x) = (2 * (sin x)) * (cos x) ; :: thesis: verum