let th1, th2 be Real; :: thesis: ( cos th1 <> 0 & sin th2 <> 0 implies (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) )
assume ( cos th1 <> 0 & sin th2 <> 0 ) ; :: thesis: (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2)))
then (tan th1) - (cot th2) = (((sin th1) * (sin th2)) - (- (- ((cos th1) * (cos th2))))) / ((cos th1) * (sin th2)) by XCMPLX_1:130
.= (- (((cos th1) * (cos th2)) - ((sin th1) * (sin th2)))) / ((cos th1) * (sin th2))
.= - ((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) / ((cos th1) * (sin th2))) by XCMPLX_1:187
.= - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) by SIN_COS:75 ;
hence (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) ; :: thesis: verum