let th1, th2 be real number ; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 implies tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) )
assume A1: ( cos th1 <> 0 & cos th2 <> 0 ) ; :: thesis: tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
then tan (th1 - th2) = ((sin (th1 + (- th2))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by XCMPLX_1:6, XCMPLX_1:55
.= ((((sin th1) * (cos (- th2))) + ((cos th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:80
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:34
.= ((((sin th1) * (cos th2)) + ((cos th1) * (- (sin th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:34
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos (- th2))) - ((sin th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) by SIN_COS:80
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos th2)) - ((sin th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) by SIN_COS:34
.= ((((sin th1) * (cos th2)) - ((cos th1) * (sin th2))) / ((cos th1) * (cos th2))) / ((((cos th1) * (cos th2)) - ((sin th1) * (- (sin th2)))) / ((cos th1) * (cos th2))) by SIN_COS:34
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) / ((cos th1) * (cos th2))) by XCMPLX_1:121
.= ((((sin th1) * (cos th2)) / ((cos th1) * (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:63
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((cos th1) * (sin th2)) / ((cos th1) * (cos th2)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:77
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) * (cos th2)) / ((cos th1) * (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:77
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) * (sin th2)) / ((cos th1) * (cos th2)))) by XCMPLX_1:77
.= ((((sin th1) / (cos th1)) * ((cos th2) / (cos th2))) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by XCMPLX_1:77
.= (((sin th1) / (cos th1)) - (((sin th2) / (cos th2)) * ((cos th1) / (cos th1)))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A1, XCMPLX_1:89
.= (((sin th1) / (cos th1)) - ((sin th2) / (cos th2))) / ((((cos th1) / (cos th1)) * ((cos th2) / (cos th2))) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A1, XCMPLX_1:89
.= (((sin th1) / (cos th1)) - ((sin th2) / (cos th2))) / (((cos th1) / (cos th1)) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A1, XCMPLX_1:89
.= ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) by A1, XCMPLX_1:60 ;
hence tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) ; :: thesis: verum