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