let x be real number ; :: thesis: ( 1 < x & 1 <= ((x ^2 ) + 1) / (2 * x) implies log number_e ,x = cosh1" (((x ^2 ) + 1) / (2 * x)) )
assume A1: ( 1 < x & 1 <= ((x ^2 ) + 1) / (2 * x) ) ; :: thesis: log number_e ,x = cosh1" (((x ^2 ) + 1) / (2 * x))
then A2: 1 * 2 < 2 * x by XREAL_1:70;
then 1 < 2 * x by XXREAL_0:2;
then A3: 1 ^2 < (2 * x) ^2 by SQUARE_1:78;
x < x ^2 by A1, SQUARE_1:76;
then 1 < x ^2 by A1, XXREAL_0:2;
then A4: 1 - 1 < (x ^2 ) - 1 by XREAL_1:16;
then A5: 0 < ((x ^2 ) - 1) ^2 by SQUARE_1:74;
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 A3, A5, SQUARE_1:99
.= log number_e ,((((x ^2 ) + 1) / (2 * x)) + (((x ^2 ) - 1) / (sqrt ((2 * x) ^2 )))) by A4, SQUARE_1:89
.= log number_e ,((((x ^2 ) + 1) / (2 * x)) + (((x ^2 ) - 1) / (2 * x))) by A2, 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)) ; :: thesis: verum