let a be Real; :: thesis: sin (3 * a) = ((4 * (sin a)) * (sin ((PI / 3) + a))) * (sin ((PI / 3) - a))
A1: ((sqrt 3) / 2) ^2 = ((sqrt 3) / 2) * ((sqrt 3) / 2) by SQUARE_1:def 1
.= (((sqrt 3) * (sqrt 3)) / 2) / 2
.= ((sqrt (3 * 3)) / 2) / 2 by SQUARE_1:29
.= ((sqrt (3 ^2)) / 2) / 2 by SQUARE_1:def 1
.= (3 / 2) / 2 by SQUARE_1:22
.= 3 / 4 ;
sin (3 * a) = (- (4 * ((sin a) |^ 3))) + (3 * (sin a)) by SIN_COS5:16
.= (((4 * (sin a)) * 3) / 4) - (4 * ((sin a) |^ (2 + 1)))
.= (((4 * (sin a)) * 3) / 4) - (4 * (((sin a) |^ 2) * (sin a))) by NEWTON:6
.= (4 * (sin a)) * ((((sqrt 3) / 2) ^2) - ((sin a) |^ 2)) by A1
.= (4 * (sin a)) * (((sin (PI / 3)) ^2) - ((sin a) ^2)) by Thm9, NEWTON:81
.= (4 * (sin a)) * (((sin (PI / 3)) - (sin a)) * ((sin (PI / 3)) + (sin a))) by SQUARE_1:8
.= ((4 * (sin a)) * ((sin (PI / 3)) + (sin a))) * ((sin (PI / 3)) - (sin a))
.= ((4 * (sin a)) * (2 * ((cos (((PI / 3) - a) / 2)) * (sin (((PI / 3) + a) / 2))))) * ((sin (PI / 3)) - (sin a)) by SIN_COS4:15
.= ((4 * (sin a)) * (2 * ((cos (((PI / 3) - a) / 2)) * (sin (((PI / 3) + a) / 2))))) * (2 * ((cos (((PI / 3) + a) / 2)) * (sin (((PI / 3) - a) / 2)))) by SIN_COS4:16
.= ((4 * (sin a)) * ((2 * (sin (((PI / 3) - a) / 2))) * (cos (((PI / 3) - a) / 2)))) * ((2 * (sin (((PI / 3) + a) / 2))) * (cos (((PI / 3) + a) / 2)))
.= ((4 * (sin a)) * (sin (2 * (((PI / 3) - a) / 2)))) * ((2 * (sin (((PI / 3) + a) / 2))) * (cos (((PI / 3) + a) / 2))) by SIN_COS5:5
.= ((4 * (sin a)) * (sin (2 * (((PI / 3) - a) / 2)))) * (sin (2 * (((PI / 3) + a) / 2))) by SIN_COS5:5
.= ((4 * (sin a)) * (sin ((PI / 3) - a))) * (sin ((PI / 3) + a)) ;
hence sin (3 * a) = ((4 * (sin a)) * (sin ((PI / 3) + a))) * (sin ((PI / 3) - a)) ; :: thesis: verum