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

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