let x be real number ; ( 0 < x & x < 1 & 1 <= ((x ^2 ) + 1) / (2 * x) implies log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x)) )
assume that
A1:
0 < x
and
A2:
x < 1
and
A3:
1 <= ((x ^2 ) + 1) / (2 * x)
; log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x))
A4:
1 / x = x to_power (- 1)
by A1, Th1;
x ^2 < x
by A1, A2, SQUARE_1:75;
then
x ^2 < 1
by A2, XXREAL_0:2;
then A5:
(x ^2 ) - (x ^2 ) < 1 - (x ^2 )
by XREAL_1:16;
0 * 2 < x * 2
by A1, A3;
then A6:
0 < (2 * x) ^2
by SQUARE_1:74;
cosh2" (((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 A6, XCMPLX_1:127
.=
- (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((sqrt ((1 - (x ^2 )) ^2 )) / (sqrt ((2 * x) ^2 )))))
by A1, A5, SQUARE_1:99
.=
- (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((1 - (x ^2 )) / (sqrt ((2 * x) ^2 )))))
by A5, SQUARE_1:89
.=
- (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((1 - (x ^2 )) / (2 * x))))
by A1, SQUARE_1:89
.=
- (log number_e ,((((x ^2 ) + 1) + (1 - (x ^2 ))) / (2 * x)))
.=
- (log number_e ,((2 * 1) / (2 * x)))
.=
- (log number_e ,(1 / x))
by XCMPLX_1:92
.=
- ((- 1) * (log number_e ,x))
by A1, A4, Lm1, POWER:63, TAYLOR_1:11
.=
log number_e ,x
;
hence
log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x))
; verum