let th1, th2, th3 be Real; ( 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 that
A1:
sin th1 <> 0
and
A2:
sin th2 <> 0
and
A3:
sin th3 <> 0
; 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)
A4:
(sin th1) * (sin th2) <> 0
by A1, A2;
cot ((th1 + th2) + th3) =
(((cos (th1 + th2)) * (cos th3)) - ((sin (th1 + th2)) * (sin th3))) / (sin ((th1 + th2) + th3))
by SIN_COS:75
.=
(((((cos th1) * (cos th2)) - ((sin th1) * (sin th2))) * (cos th3)) - ((sin (th1 + th2)) * (sin th3))) / (sin ((th1 + th2) + th3))
by SIN_COS:75
.=
(((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:75
.=
((((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 A3, A4, 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:120
.=
(((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:76
.=
(((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:120
.=
(((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:76
.=
(((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, A2, 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 A3, XCMPLX_1:91
.=
(((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:62
.=
(((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:91
.=
(((cot th3) * (((cot th1) * (cot th2)) - 1)) - ((cot th2) + ((cos th1) / (sin th1)))) / ((sin ((th1 + th2) + th3)) / (((sin th1) * (sin th2)) * (sin th3)))
by A2, XCMPLX_1:91
.=
((((((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:75
.=
((((((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:62
.=
((((((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 A3, XCMPLX_1:91
.=
((((((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:76
.=
((((((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:75
.=
((((((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:62
.=
((((((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:91
.=
((((((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 A2, XCMPLX_1:91
.=
((((((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:75
.=
((((((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:120
.=
((((((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, A2, 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:76
.=
((((((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)
; verum