let x be Real; :: thesis: ( x >= 0 implies tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) )
assume A1: x >= 0 ; :: thesis: tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1))
A2: ( (cosh x) + 1 > 0 & (cosh x) - 1 >= 0 ) by Lm13;
tanh (x / 2) = (sinh (x / 2)) / (cosh (x / 2)) by Th1
.= (sqrt (((cosh x) - 1) / 2)) / (cosh (x / 2)) by A1, Th24
.= (sqrt (((cosh x) - 1) / 2)) / (sqrt (((cosh x) + 1) / 2)) by SIN_COS5:48
.= sqrt ((((cosh x) - 1) / 2) / (((cosh x) + 1) / 2)) by A2, SQUARE_1:30
.= sqrt (((cosh x) - 1) / ((cosh x) + 1)) by XCMPLX_1:55 ;
hence tanh (x / 2) = sqrt (((cosh x) - 1) / ((cosh x) + 1)) ; :: thesis: verum