let x1, x2 be Real; :: thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) ) )
assume that
A1: sinh x1 <> 0 and
A2: sinh x2 <> 0 ; :: thesis: ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) )
A3: sinh . x1 <> 0 by A1, SIN_COS2:def 2;
A4: sinh . x2 <> 0 by A2, SIN_COS2:def 2;
A5: - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) = - ((sinh . (x1 - x2)) / ((sinh x1) * (sinh x2))) by SIN_COS2:def 2
.= - ((sinh . (x1 - x2)) / ((sinh . x1) * (sinh x2))) by SIN_COS2:def 2
.= - ((sinh . (x1 - x2)) / ((sinh . x1) * (sinh . x2))) by SIN_COS2:def 2
.= - ((((sinh . x1) * (cosh . x2)) - ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by SIN_COS2:21
.= - ((((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) - (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:120
.= - (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) - (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:83
.= - (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x1)) / (sinh . x1))) by XCMPLX_1:83
.= - (((1 * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x1)) / (sinh . x1))) by A3, XCMPLX_1:60
.= - (((cosh . x2) / (sinh . x2)) - ((1 * (cosh . x1)) / (sinh . x1))) by A4, XCMPLX_1:60
.= - (((cosh x2) / (sinh . x2)) - ((cosh . x1) / (sinh . x1))) by SIN_COS2:def 4
.= - (((cosh x2) / (sinh . x2)) - ((cosh x1) / (sinh . x1))) by SIN_COS2:def 4
.= - (((cosh x2) / (sinh x2)) - ((cosh x1) / (sinh . x1))) by SIN_COS2:def 2
.= - ((coth x2) - ((cosh x1) / (sinh x1))) by SIN_COS2:def 2
.= (coth x1) - (coth x2) ;
(sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) = (sinh . (x1 + x2)) / ((sinh x1) * (sinh x2)) by SIN_COS2:def 2
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh x1) * (sinh x2)) by SIN_COS2:21
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh x2)) by SIN_COS2:def 2
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2)) by SIN_COS2:def 2
.= (((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:62
.= ((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:83
.= ((1 * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by A3, XCMPLX_1:60
.= ((cosh . x2) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2)) by XCMPLX_1:83
.= ((cosh . x2) / (sinh . x2)) + (((cosh . x1) / (sinh . x1)) * ((sinh . x2) / (sinh . x2))) by XCMPLX_1:74
.= ((cosh . x2) / (sinh . x2)) + (((cosh . x1) / (sinh . x1)) * 1) by A4, XCMPLX_1:60
.= ((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def 2
.= ((cosh . x2) / (sinh x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def 2
.= ((cosh x2) / (sinh x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def 4
.= (coth x2) + (coth x1) by SIN_COS2:def 4 ;
hence ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) ) by A5; :: thesis: verum