let x be real number ; :: 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)))
(cosh x) + 1 > 0 by Lm13;
then A2: ((cosh x) + 1) / 2 > 0 by XREAL_1:141;
(cosh x) - 1 >= 0 by Lm13;
then A3: ((cosh x) - 1) / 2 >= 0 / 2 ;
tanh (x / 2) = (sinh (x / 2)) / (cosh (x / 2)) by Th1
.= (- (sqrt (((cosh x) - 1) / 2))) / (cosh (x / 2)) by A1, Th25
.= - ((sqrt (((cosh x) - 1) / 2)) / (cosh (x / 2))) by XCMPLX_1:188
.= - ((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, A3, SQUARE_1:99
.= - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) by XCMPLX_1:55 ;
hence tanh (x / 2) = - (sqrt (((cosh x) - 1) / ((cosh x) + 1))) ; :: thesis: verum