let th1, th2 be Real; :: thesis: ( cos th1 <> 0 & cos th2 <> 0 implies tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2))) )
assume that
A1: cos th1 <> 0 and
A2: cos th2 <> 0 ; :: thesis: tan (th1 - th2) = ((tan th1) - (tan th2)) / (1 + ((tan th1) * (tan th2)))
tan (th1 - th2) = ((sin (th1 + (- th2))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by A1, A2, 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:75
.= ((((sin th1) * (cos th2)) + ((cos th1) * (sin (- th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((sin th1) * (cos th2)) + ((cos th1) * (- (sin th2)))) / ((cos th1) * (cos th2))) / ((cos (th1 + (- th2))) / ((cos th1) * (cos th2))) by SIN_COS:31
.= ((((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:75
.= ((((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:31
.= ((((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:31
.= ((((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:120
.= ((((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:62
.= ((((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:76
.= ((((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:76
.= ((((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:76
.= ((((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:76
.= (((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 A2, XCMPLX_1:88
.= (((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:88
.= (((sin th1) / (cos th1)) - ((sin th2) / (cos th2))) / (((cos th1) / (cos th1)) + (((sin th1) / (cos th1)) * ((sin th2) / (cos th2)))) by A2, XCMPLX_1:88
.= ((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