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