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