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)))
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, Th25
.= - ((sqrt (((cosh x) - 1) / 2)) / (cosh (x / 2))) by XCMPLX_1:187
.= - ((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