let x be real number ; ( x > 0 & x < 1 implies tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 )))) )
assume that
A1:
x > 0
and
A2:
x < 1
; tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2 )) / (1 - (x ^2 ))))
A3:
0 < (1 - (x ^2 )) ^2
by A1, A2, Th19;
A4:
(2 * x) / (1 - (x ^2 )) > 0
by A1, A2, Th18;
(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 A3, 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 A4, 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 ))))
; verum