let y, z be Real; :: 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 A1: 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)) )
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:91
.= (((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, Lm4, XCMPLX_1:91
.= (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:120
.= (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:91
.= (((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, Lm4, XCMPLX_1:91
.= (((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) by XCMPLX_1:62
.= (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