let x be real number ; :: thesis: ( 0 < x & ((x - 1) / (x + 1)) ^2 < 1 implies log number_e ,x = 2 * (tanh" ((x - 1) / (x + 1))) )
assume ( 0 < x & ((x - 1) / (x + 1)) ^2 < 1 ) ; :: thesis: log number_e ,x = 2 * (tanh" ((x - 1) / (x + 1)))
then A1: x + 1 > 0 ;
then 2 * (tanh" ((x - 1) / (x + 1))) = log number_e ,((((x - 1) + ((x + 1) * 1)) / (x + 1)) / (1 - ((x - 1) / (x + 1)))) by XCMPLX_1:114
.= log number_e ,(((2 * x) / (x + 1)) / (((1 * (x + 1)) - (x - 1)) / (x + 1))) by A1, XCMPLX_1:128
.= log number_e ,((2 * x) / 2) by A1, XCMPLX_1:55
.= log number_e ,x ;
hence log number_e ,x = 2 * (tanh" ((x - 1) / (x + 1))) ; :: thesis: verum