let x1, x2 be real number ; :: thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2)) )
assume ( sinh x1 <> 0 & sinh x2 <> 0 ) ; :: thesis: coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
then A1: ( sinh . x1 <> 0 & sinh . x2 <> 0 ) by SIN_COS2:def 2;
coth (x1 + x2) = (cosh . (x1 + x2)) / (sinh (x1 + x2)) by SIN_COS2:def 4
.= (cosh . (x1 + x2)) / (sinh . (x1 + x2)) by SIN_COS2:def 2
.= (((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / (sinh . (x1 + x2)) by SIN_COS2:20
.= (((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) by SIN_COS2:21
.= ((((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by A1, XCMPLX_1:6, XCMPLX_1:55
.= ((((cosh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((sinh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:63
.= ((((cosh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by A1, XCMPLX_1:6, XCMPLX_1:60
.= (((((cosh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:84
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:75
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:63
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:84
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2))) by XCMPLX_1:84
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((1 * (cosh . x2)) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2))) by A1, XCMPLX_1:60
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by A1, XCMPLX_1:90
.= ((((cosh x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def 4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def 4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def 4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def 4
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def 2
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def 2
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x1) / (sinh x1))) by SIN_COS2:def 2
.= (((coth x1) * (coth x2)) + 1) / ((coth x2) + (coth x1)) by SIN_COS2:def 2 ;
hence coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2)) ; :: thesis: verum