let x be Real; ( 1 < x implies log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x)) )
assume A1:
1 < x
; log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x))
then
x < x ^2
by SQUARE_1:14;
then
1 < x ^2
by A1, XXREAL_0:2;
then A2:
1 - 1 < (x ^2) - 1
by XREAL_1:14;
1 * 2 < 2 * x
by A1, XREAL_1:68;
then
1 < 2 * x
by XXREAL_0:2;
then A3:
1 ^2 < (2 * x) ^2
by SQUARE_1:16;
cosh1" (((x ^2) + 1) / (2 * x)) =
log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt (((((x ^2) + 1) ^2) / ((2 * x) ^2)) - 1))))
by XCMPLX_1:76
.=
log (number_e,((((x ^2) + 1) / (2 * x)) + (sqrt ((((((x ^2) ^2) + (2 * (x ^2))) + 1) - (1 * ((2 * x) ^2))) / ((2 * x) ^2)))))
by A3, XCMPLX_1:126
.=
log (number_e,((((x ^2) + 1) / (2 * x)) + ((sqrt (((x ^2) - 1) ^2)) / (sqrt ((2 * x) ^2)))))
by A1, A2, SQUARE_1:30
.=
log (number_e,((((x ^2) + 1) / (2 * x)) + (((x ^2) - 1) / (sqrt ((2 * x) ^2)))))
by A2, SQUARE_1:22
.=
log (number_e,((((x ^2) + 1) / (2 * x)) + (((x ^2) - 1) / (2 * x))))
by A1, SQUARE_1:22
.=
log (number_e,((((x ^2) + 1) + ((x ^2) - 1)) / (2 * x)))
.=
log (number_e,((2 * (x ^2)) / (2 * x)))
.=
log (number_e,((x * x) / x))
by XCMPLX_1:91
.=
log (number_e,(x / (x / x)))
by XCMPLX_1:77
.=
log (number_e,(x / 1))
by A1, XCMPLX_1:60
.=
log (number_e,x)
;
hence
log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x))
; verum