let y, z be real number ; :: thesis: ( y <> 0 implies ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) )
assume y <> 0 ; :: thesis: ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) )
then A1: sinh y <> 0 by Lm4;
A2: cosh z <> 0 by Lm1;
A3: (coth y) + (tanh z) = ((cosh y) / (sinh y)) + (tanh z) by SIN_COS5:def 1
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (tanh z) by A2, XCMPLX_1:92
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + ((sinh z) / (cosh z)) by Th1
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) by A1, XCMPLX_1:92
.= (((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:63
.= (cosh (y + z)) / ((sinh y) * (cosh z)) by Lm10 ;
(coth y) - (tanh z) = ((cosh y) / (sinh y)) - (tanh z) by SIN_COS5:def 1
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (tanh z) by A2, XCMPLX_1:92
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - ((sinh z) / (cosh z)) by Th1
.= (((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) by A1, XCMPLX_1:92
.= (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:121
.= (cosh (y - z)) / ((sinh y) * (cosh z)) by Lm10 ;
hence ( (coth y) + (tanh z) = (cosh (y + z)) / ((sinh y) * (cosh z)) & (coth y) - (tanh z) = (cosh (y - z)) / ((sinh y) * (cosh z)) ) by A3; :: thesis: verum