let th1, th2 be Real; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 implies (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) )
assume A1: ( cos th1 <> 0 & cos th2 <> 0 ) ; :: thesis: (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2)))
(cos (th1 + th2)) / (cos (th1 - th2)) = (((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / (cos (th1 - th2)) by SIN_COS:75
.= ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by A1, XCMPLX_1:55
.= ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by XCMPLX_1:120
.= (1 - (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by A1, XCMPLX_1:60
.= (1 - ((tan th1) * ((sin th2) / (cos th2)))) / ((cos (th1 - th2)) / ((cos th1) * (cos th2))) by XCMPLX_1:76
.= (1 - ((tan th1) * (tan th2))) / ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by SIN_COS:83
.= (1 - ((tan th1) * (tan th2))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:62
.= (1 - ((tan th1) * (tan th2))) / (1 + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by A1, XCMPLX_1:60
.= (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) by XCMPLX_1:76 ;
hence (cos (th1 + th2)) / (cos (th1 - th2)) = (1 - ((tan th1) * (tan th2))) / (1 + ((tan th1) * (tan th2))) ; :: thesis: verum