let x be Real; ( 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:76
.=
(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:126
.=
(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:76
.=
(1 / 2) * (log (number_e,(((1 + (x ^2)) / (1 - (x ^2))) + ((2 * x) / (1 - (x ^2))))))
by A4, SQUARE_1:22
.=
(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:91
;
hence
tanh" x = (1 / 2) * (cosh1" ((1 + (x ^2)) / (1 - (x ^2))))
; verum