let x be Real; :: thesis: ( sinh (x / 2) <> 0 implies coth (x / 2) = (sinh x) / ((cosh x) - 1) )
assume sinh (x / 2) <> 0 ; :: thesis: coth (x / 2) = (sinh x) / ((cosh x) - 1)
then A1: 2 * (sinh . (x / 2)) <> 0 by SIN_COS2:def 2;
(sinh x) / ((cosh x) - 1) = (sinh . (2 * (x / 2))) / ((cosh (2 * (x / 2))) - 1) by SIN_COS2:def 2
.= (sinh . (2 * (x / 2))) / ((cosh . (2 * (x / 2))) - 1) by SIN_COS2:def 4
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((cosh . (2 * (x / 2))) - 1) by SIN_COS2:23
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (((2 * ((cosh . (x / 2)) ^2)) - 1) - 1) by SIN_COS2:23
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * (((cosh . (x / 2)) ^2) - 1))
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * ((sinh . (x / 2)) ^2)) by Lm3
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((2 * (sinh . (x / 2))) * (sinh . (x / 2)))
.= (cosh . (x / 2)) / (sinh . (x / 2)) by A1, XCMPLX_1:91
.= (cosh (x / 2)) / (sinh . (x / 2)) by SIN_COS2:def 4
.= (cosh (x / 2)) / (sinh (x / 2)) by SIN_COS2:def 2 ;
hence coth (x / 2) = (sinh x) / ((cosh x) - 1) ; :: thesis: verum