let x be real number ; :: thesis: ( x > 1 implies cosh1" x = tanh" ((sqrt ((x ^2 ) - 1)) / x) )
assume A1: x > 1 ; :: thesis: cosh1" x = tanh" ((sqrt ((x ^2 ) - 1)) / x)
then x ^2 > (1 ^2 ) + 0 by SQUARE_1:78;
then A2: (x ^2 ) - 1 > 0 by XREAL_1:22;
then A3: ( sqrt ((x ^2 ) - 1) > 0 & ((sqrt ((x ^2 ) - 1)) / x) ^2 < 1 & (sqrt ((x ^2 ) - 1)) + x > 0 ) by A1, Th2, Th23, SQUARE_1:93;
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 A3, 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 A2, 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 A3, Lm2, POWER:63
.= log number_e ,((sqrt ((x ^2 ) - 1)) + x) ;
hence cosh1" x = tanh" ((sqrt ((x ^2 ) - 1)) / x) ; :: thesis: verum