let th1, th2, th3 be Real; :: thesis: ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3)))
((sin th1) * (cos th2)) * (cos th3) = ((1 / 2) * ((sin (th1 + th2)) + (sin (th1 - th2)))) * (cos th3) by Th30
.= (1 / 2) * (((sin (th1 + th2)) * (cos th3)) + ((sin (th1 - th2)) * (cos th3)))
.= (1 / 2) * (((1 / 2) * ((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3)))) + ((sin (th1 - th2)) * (cos th3))) by Th30
.= (1 / 2) * (((1 / 2) * ((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3)))) + ((1 / 2) * ((sin ((th1 - th2) + th3)) + (sin ((th1 - th2) - th3))))) by Th30
.= (1 / (2 * 2)) * (((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3))) + ((sin ((th1 + (- th2)) + th3)) + (sin (- ((th2 - th1) + th3)))))
.= (1 / (2 * 2)) * (((sin ((th1 + th2) + th3)) + (sin ((th1 + th2) - th3))) + ((- (sin ((th2 - th1) + th3))) + (sin ((th3 + th1) + (- th2))))) by SIN_COS:31
.= (1 / (2 * 2)) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3))) ;
hence ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3))) ; :: thesis: verum