let x1, x2 be Real; ( sinh x1 <> 0 & sinh x2 <> 0 implies coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2)) )
assume that
A1:
sinh x1 <> 0
and
A2:
sinh x2 <> 0
; coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
A3:
sinh . x1 <> 0
by A1, SIN_COS2:def 2;
A4:
sinh . x2 <> 0
by A2, 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 A3, A4, 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:62
.=
((((cosh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2)))
by A3, A4, 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:83
.=
((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2)))
by XCMPLX_1:74
.=
((((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:62
.=
((((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:83
.=
((((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:83
.=
((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((1 * (cosh . x2)) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2)))
by A3, XCMPLX_1:60
.=
((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1)))
by A4, XCMPLX_1:89
.=
((((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))
; verum