let x be real number ; ( x > 1 implies cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x) )
assume A1:
x > 1
; cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x)
then A2:
(sqrt ((x ^2) - 1)) + x > 0
by Th23;
x ^2 > (1 ^2) + 0
by A1, SQUARE_1:78;
then A3:
(x ^2) - 1 > 0
by XREAL_1:22;
tanh" ((sqrt ((x ^2) - 1)) / x) =
(1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + (x * 1)) / x) / (1 - ((sqrt ((x ^2) - 1)) / x)))))
by A1, XCMPLX_1:114
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) / x) / (((1 * x) - (sqrt ((x ^2) - 1))) / x))))
by A1, XCMPLX_1:128
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) / (x - (sqrt ((x ^2) - 1))))))
by A1, XCMPLX_1:55
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x - (sqrt ((x ^2) - 1))) * ((sqrt ((x ^2) - 1)) + x)))))
by A2, XCMPLX_1:92
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x ^2) - ((sqrt ((x ^2) - 1)) ^2)))))
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) - 1)) + x) * ((sqrt ((x ^2) - 1)) + x)) / ((x ^2) - ((x ^2) - 1)))))
by A3, SQUARE_1:def 4
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) ^2)))
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) - 1)) + x) to_power 2)))
by POWER:53
.=
(1 / 2) * (2 * (log (number_e,((sqrt ((x ^2) - 1)) + x))))
by A2, Lm1, POWER:63, TAYLOR_1:11
.=
log (number_e,((sqrt ((x ^2) - 1)) + x))
;
hence
cosh1" x = tanh" ((sqrt ((x ^2) - 1)) / x)
; verum