let x be real number ; :: thesis: ( 0 < x implies log number_e ,x = tanh" (((x ^2 ) - 1) / ((x ^2 ) + 1)) )
assume A1: 0 < x ; :: thesis: log number_e ,x = tanh" (((x ^2 ) - 1) / ((x ^2 ) + 1))
A2: (x ^2 ) + 1 > 0 by Lm6;
then tanh" (((x ^2 ) - 1) / ((x ^2 ) + 1)) = (1 / 2) * (log number_e ,(((((x ^2 ) - 1) + (((x ^2 ) + 1) * 1)) / ((x ^2 ) + 1)) / (1 - (((x ^2 ) - 1) / ((x ^2 ) + 1))))) by XCMPLX_1:114
.= (1 / 2) * (log number_e ,(((2 * (x ^2 )) / ((x ^2 ) + 1)) / (((1 * ((x ^2 ) + 1)) - ((x ^2 ) - 1)) / ((x ^2 ) + 1)))) by A2, XCMPLX_1:128
.= (1 / 2) * (log number_e ,((2 * (x ^2 )) / 2)) by A2, XCMPLX_1:55
.= (1 / 2) * (log number_e ,(x to_power 2)) by POWER:53
.= (1 / 2) * (2 * (log number_e ,x)) by A1, Lm1, POWER:63, TAYLOR_1:11
.= log number_e ,x ;
hence log number_e ,x = tanh" (((x ^2 ) - 1) / ((x ^2 ) + 1)) ; :: thesis: verum