let x be real number ; ( 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:76;
then
1 < x ^2
by A1, XXREAL_0:2;
then A2:
1 - 1 < (x ^2 ) - 1
by XREAL_1:16;
1 * 2 < 2 * x
by A1, XREAL_1:70;
then
1 < 2 * x
by XXREAL_0:2;
then A3:
1 ^2 < (2 * x) ^2
by SQUARE_1:78;
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:77
.=
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:127
.=
log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((sqrt (((x ^2 ) - 1) ^2 )) / (sqrt ((2 * x) ^2 ))))
by A1, A2, SQUARE_1:99
.=
log number_e ,((((x ^2 ) + 1) / (2 * x)) + (((x ^2 ) - 1) / (sqrt ((2 * x) ^2 ))))
by A2, SQUARE_1:89
.=
log number_e ,((((x ^2 ) + 1) / (2 * x)) + (((x ^2 ) - 1) / (2 * x)))
by A1, SQUARE_1:89
.=
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:92
.=
log number_e ,(x / (x / x))
by XCMPLX_1:78
.=
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