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