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