let x be real number ; ( 0 < x & x < 1 implies tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 )))) )
assume that
A1:
0 < x
and
A2:
x < 1
; tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 ))))
A3:
1 - (x ^2 ) > 0
by A1, A2, Lm5;
A4:
(1 + x) / (1 - x) > 0
by A1, A2, Th15;
A5:
1 - x > 0
by A2, XREAL_1:52;
A6:
sqrt (1 + x) > 0
by A1, SQUARE_1:93;
(1 + x) / (1 - x) > 0
by A1, A2, Th15;
then A7:
sqrt ((1 + x) / (1 - x)) = ((1 + x) / (1 - x)) to_power (1 / 2)
by ASYMPT_1:89;
A8:
x ^2 >= 0
by XREAL_1:65;
cosh1" (1 / (sqrt (1 - (x ^2 )))) =
log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 / ((sqrt (1 - (x ^2 ))) ^2 )) - (1 ^2 ))))
by XCMPLX_1:77
.=
log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 / (1 - (x ^2 ))) - 1)))
by A3, SQUARE_1:def 4
.=
log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 - (1 * (1 - (x ^2 )))) / (1 - (x ^2 )))))
by A3, XCMPLX_1:127
.=
log number_e ,((1 / (sqrt (1 - (x ^2 )))) + ((sqrt (x ^2 )) / (sqrt (1 - (x ^2 )))))
by A3, A8, SQUARE_1:99
.=
log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (x / (sqrt (1 - (x ^2 )))))
by A1, SQUARE_1:89
.=
log number_e ,((1 + x) / (sqrt ((1 - x) * (1 + x))))
.=
log number_e ,((1 + x) / ((sqrt (1 - x)) * (sqrt (1 + x))))
by A1, A5, SQUARE_1:97
.=
log number_e ,((sqrt ((1 + x) ^2 )) / ((sqrt (1 - x)) * (sqrt (1 + x))))
by A1, SQUARE_1:89
.=
log number_e ,(((sqrt (1 + x)) * (sqrt (1 + x))) / ((sqrt (1 - x)) * (sqrt (1 + x))))
by A1, SQUARE_1:97
.=
log number_e ,((sqrt (1 + x)) / (sqrt (1 - x)))
by A6, XCMPLX_1:92
.=
log number_e ,(sqrt ((1 + x) / (1 - x)))
by A1, A5, SQUARE_1:99
.=
(1 / 2) * (log number_e ,((1 + x) / (1 - x)))
by A7, A4, Lm1, POWER:63, TAYLOR_1:11
;
hence
tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 ))))
; verum