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