let th1, th2 be real number ; :: 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:131
.= (- (((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:188
.= - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) by SIN_COS:80 ;
hence (tan th1) - (cot th2) = - ((cos (th1 + th2)) / ((cos th1) * (sin th2))) ; :: thesis: verum