let x be Real; :: thesis: ( x <> 0 implies ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) )
assume x <> 0 ; :: thesis: ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) )
then A1: x / 2 <> 0 ;
A2: (coth (x / 2)) - 1 = (1 / (1 / (coth (x / 2)))) - 1 by XCMPLX_1:56
.= (1 / (tanh (x / 2))) - 1 by Th2
.= (1 / (tanh (x / 2))) - ((tanh (x / 2)) / (tanh (x / 2))) by A1, Lm4, XCMPLX_1:60
.= (1 - (tanh (x / 2))) / (tanh (x / 2)) by XCMPLX_1:120 ;
A3: (coth (x / 2)) + 1 = (1 / (1 / (coth (x / 2)))) + 1 by XCMPLX_1:56
.= (1 / (tanh (x / 2))) + 1 by Th2
.= (1 / (tanh (x / 2))) + ((tanh (x / 2)) / (tanh (x / 2))) by A1, Lm4, XCMPLX_1:60
.= (1 + (tanh (x / 2))) / (tanh (x / 2)) by XCMPLX_1:62 ;
A4: exp_R (- x) = (1 - (tanh (x / 2))) / (1 + (tanh (x / 2))) by Th7
.= ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) by A1, A3, A2, Lm4, XCMPLX_1:55 ;
exp_R x = (1 + (tanh (x / 2))) / (1 - (tanh (x / 2))) by Th7
.= ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) by A1, A3, A2, Lm4, XCMPLX_1:55 ;
hence ( exp_R x = ((coth (x / 2)) + 1) / ((coth (x / 2)) - 1) & exp_R (- x) = ((coth (x / 2)) - 1) / ((coth (x / 2)) + 1) ) by A4; :: thesis: verum