let x be Real; ( 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
1 <= ((x ^2) + 1) / (2 * x)
; log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x))
A3:
1 / x = x to_power (- 1)
by A1, Th1;
x ^2 < x
by A1, A2, SQUARE_1:13;
then
x ^2 < 1
by A2, XXREAL_0:2;
then A4:
(x ^2) - (x ^2) < 1 - (x ^2)
by XREAL_1:14;
0 * 2 < x * 2
by A1;
then A5:
0 < (2 * x) ^2
;
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: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 A5, XCMPLX_1:126
.=
- (log (number_e,((((x ^2) + 1) / (2 * x)) + ((sqrt ((1 - (x ^2)) ^2)) / (sqrt ((2 * x) ^2))))))
by A1, A4, SQUARE_1:30
.=
- (log (number_e,((((x ^2) + 1) / (2 * x)) + ((1 - (x ^2)) / (sqrt ((2 * x) ^2))))))
by A4, SQUARE_1:22
.=
- (log (number_e,((((x ^2) + 1) / (2 * x)) + ((1 - (x ^2)) / (2 * x)))))
by A1, SQUARE_1:22
.=
- (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:91
.=
- ((- 1) * (log (number_e,x)))
by A1, A3, Lm1, POWER:55, TAYLOR_1:11
.=
log (number_e,x)
;
hence
log (number_e,x) = cosh2" (((x ^2) + 1) / (2 * x))
; verum