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