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