let x be real number ; :: thesis: ( x > 0 & x < 1 implies tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 )))) )
assume ( x > 0 & x < 1 ) ; :: thesis: tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 ))))
then A1: ( 0 < x + 1 & x ^2 < 1 & 0 < 1 - (x ^2 ) & 0 < (1 - (x ^2 )) ^2 & (2 * x) / (1 - (x ^2 )) > 0 & (1 + (x ^2 )) / (1 - (x ^2 )) > 1 ) by Lm7, Th16, Th18, Th19, Th20;
(1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 )))) = (1 / 2) * (log number_e ,(((1 + (x ^2 )) / (1 - (x ^2 ))) + (sqrt ((((1 + (x ^2 )) ^2 ) / ((1 - (x ^2 )) ^2 )) - 1)))) by XCMPLX_1:77
.= (1 / 2) * (log number_e ,(((1 + (x ^2 )) / (1 - (x ^2 ))) + (sqrt ((((1 + (x ^2 )) ^2 ) - (1 * ((1 - (x ^2 )) ^2 ))) / ((1 - (x ^2 )) ^2 ))))) by A1, XCMPLX_1:127
.= (1 / 2) * (log number_e ,(((1 + (x ^2 )) / (1 - (x ^2 ))) + (sqrt (((2 * x) ^2 ) / ((1 - (x ^2 )) ^2 )))))
.= (1 / 2) * (log number_e ,(((1 + (x ^2 )) / (1 - (x ^2 ))) + (sqrt (((2 * x) / (1 - (x ^2 ))) ^2 )))) by XCMPLX_1:77
.= (1 / 2) * (log number_e ,(((1 + (x ^2 )) / (1 - (x ^2 ))) + ((2 * x) / (1 - (x ^2 ))))) by A1, SQUARE_1:89
.= (1 / 2) * (log number_e ,(((1 + (x ^2 )) + (2 * x)) / (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) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 )))) ; :: thesis: verum