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 A1: ( 0 < x & x < 1 & 1 <= ((x ^2 ) + 1) / (2 * x) ) ; :: thesis: log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x))
then A2: 0 * 2 < x * 2 ;
then A3: 0 < (2 * x) ^2 by SQUARE_1:74;
x ^2 < x by A1, SQUARE_1:75;
then x ^2 < 1 by A1, XXREAL_0:2;
then A4: (x ^2 ) - (x ^2 ) < 1 - (x ^2 ) by XREAL_1:16;
then A5: 0 < (1 - (x ^2 )) ^2 by SQUARE_1:74;
A6: 1 / x = x to_power (- 1) by A1, Th1;
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 A3, XCMPLX_1:127
.= - (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((sqrt ((1 - (x ^2 )) ^2 )) / (sqrt ((2 * x) ^2 ))))) by A3, A5, SQUARE_1:99
.= - (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((1 - (x ^2 )) / (sqrt ((2 * x) ^2 ))))) by A4, SQUARE_1:89
.= - (log number_e ,((((x ^2 ) + 1) / (2 * x)) + ((1 - (x ^2 )) / (2 * x)))) by A2, 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, A6, Lm2, POWER:63
.= log number_e ,x ;
hence log number_e ,x = cosh2" (((x ^2 ) + 1) / (2 * x)) ; :: thesis: verum