let x be real number ; :: thesis: ( x ^2 < 1 implies tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2 )))) )
assume x ^2 < 1 ; :: thesis: tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2 ))))
then A1: ( (1 - (x ^2 )) ^2 > 0 & ((x ^2 ) + 1) / (1 - (x ^2 )) >= 0 & x + 1 > 0 & 1 - x > 0 ) by Th11, Th12, Th13;
(1 / 2) * (sinh" ((2 * x) / (1 - (x ^2 )))) = (1 / 2) * (log number_e ,(((2 * x) / (1 - (x ^2 ))) + (sqrt ((((2 * x) ^2 ) / ((1 - (x ^2 )) ^2 )) + 1)))) by XCMPLX_1:77
.= (1 / 2) * (log number_e ,(((2 * x) / (1 - (x ^2 ))) + (sqrt (((4 * (x ^2 )) + (((1 - (x ^2 )) ^2 ) * 1)) / ((1 - (x ^2 )) ^2 ))))) by A1, XCMPLX_1:114
.= (1 / 2) * (log number_e ,(((2 * x) / (1 - (x ^2 ))) + (sqrt ((((x ^2 ) + 1) ^2 ) / ((1 - (x ^2 )) ^2 )))))
.= (1 / 2) * (log number_e ,(((2 * x) / (1 - (x ^2 ))) + (sqrt ((((x ^2 ) + 1) / (1 - (x ^2 ))) ^2 )))) by XCMPLX_1:77
.= (1 / 2) * (log number_e ,(((2 * x) / (1 - (x ^2 ))) + (((x ^2 ) + 1) / (1 - (x ^2 ))))) by A1, SQUARE_1:89
.= (1 / 2) * (log number_e ,(((2 * x) + ((x ^2 ) + 1)) / (1 - (x ^2 ))))
.= (1 / 2) * (log number_e ,(((x + 1) * (x + 1)) / ((1 - x) * (1 + x))))
.= (1 / 2) * (log number_e ,((x + 1) / (1 - x))) by A1, XCMPLX_1:92 ;
hence tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2 )))) ; :: thesis: verum