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