let x be real number ; :: thesis: ( cosh (x / 2) <> 0 implies coth (x / 2) = ((cosh x) + 1) / (sinh x) )
assume cosh (x / 2) <> 0 ; :: thesis: coth (x / 2) = ((cosh x) + 1) / (sinh x)
then A1: 2 * (cosh . (x / 2)) <> 0 by SIN_COS2:def 4;
((cosh x) + 1) / (sinh x) = ((cosh . (2 * (x / 2))) + 1) / (sinh (2 * (x / 2))) by SIN_COS2:def 4
.= (((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / (sinh (2 * (x / 2))) by SIN_COS2:23
.= (2 * ((cosh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) by SIN_COS2:def 2
.= (2 * ((cosh . (x / 2)) * (cosh . (x / 2)))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) by SIN_COS2:23
.= ((2 * (cosh . (x / 2))) * (cosh . (x / 2))) / ((2 * (cosh . (x / 2))) * (sinh . (x / 2)))
.= (cosh . (x / 2)) / (sinh . (x / 2)) by A1, XCMPLX_1:92
.= (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) = ((cosh x) + 1) / (sinh x) ; :: thesis: verum