let x be real number ; :: thesis: ( sinh (x / 2) <> 0 implies tanh (x / 2) = ((cosh x) - 1) / (sinh x) )
assume sinh (x / 2) <> 0 ; :: thesis: tanh (x / 2) = ((cosh x) - 1) / (sinh x)
then A1: 2 * (sinh . (x / 2)) <> 0 by SIN_COS2:def 2;
((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) - 1)) / (sinh (2 * (x / 2)))
.= (2 * ((sinh . (x / 2)) ^2)) / (sinh (2 * (x / 2))) by Lm3
.= (2 * ((sinh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) by SIN_COS2:def 2
.= ((2 * (sinh . (x / 2))) * (sinh . (x / 2))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) by SIN_COS2:23
.= (sinh . (x / 2)) / (cosh . (x / 2)) by A1, XCMPLX_1:91
.= tanh . (x / 2) by SIN_COS2:17
.= tanh (x / 2) by SIN_COS2:def 6 ;
hence tanh (x / 2) = ((cosh x) - 1) / (sinh x) ; :: thesis: verum