let th1, th2, th3 be Real; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 implies sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 and
A3: cos th3 <> 0 ; :: thesis: sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))
sin ((th1 + th2) + th3) = sin (th1 + (th2 + th3))
.= ((sin th1) * (cos (th2 + th3))) + ((cos th1) * (sin (th2 + th3))) by SIN_COS:75
.= ((sin th1) * (((cos th2) * (cos th3)) - ((sin th2) * (sin th3)))) + ((cos th1) * (sin (th2 + th3))) by SIN_COS:75
.= (((sin th1) * ((cos th2) * (cos th3))) - ((sin th1) * ((sin th2) * (sin th3)))) + ((cos th1) * (((sin th2) * (cos th3)) + ((cos th2) * (sin th3)))) by SIN_COS:75
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - ((sin th1) * ((sin th2) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A1, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * ((sin th2) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A1, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * (sin th3)))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A2, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) + (((cos th1) * ((sin th2) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A3, Th6
.= ((((cos th1) * (tan th1)) * ((cos th2) * (cos th3))) - (((cos th1) * (tan th1)) * (((cos th2) * (tan th2)) * ((cos th3) * (tan th3))))) + (((cos th1) * (((cos th2) * (tan th2)) * (cos th3))) + ((cos th1) * ((cos th2) * (sin th3)))) by A2, Th6
.= ((((cos th1) * (cos th2)) * ((cos th3) * (tan th1))) - ((((cos th1) * (cos th2)) * ((tan th1) * (tan th2))) * ((cos th3) * (tan th3)))) + (((cos th1) * (((cos th2) * (tan th2)) * (cos th3))) + ((cos th1) * ((cos th2) * ((cos th3) * (tan th3))))) by A3, Th6
.= (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) ;
hence sin ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) ; :: thesis: verum