let x be real number ; :: thesis: ( 0 < x implies log number_e ,x = sinh" (((x ^2 ) - 1) / (2 * x)) )
assume A1: 0 < x ; :: thesis: log number_e ,x = sinh" (((x ^2 ) - 1) / (2 * x))
then A2: 0 * 2 < x * 2 by XREAL_1:70;
then A3: 0 < (2 * x) ^2 by SQUARE_1:74;
x ^2 >= 0 by XREAL_1:65;
then A4: (x ^2 ) + 1 >= 0 + 1 by XREAL_1:9;
then A5: ((x ^2 ) + 1) ^2 > 0 by SQUARE_1:74;
sinh" (((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) + (((2 * x) ^2 ) * 1)) / ((2 * x) ^2 )))) by A3, XCMPLX_1:114
.= 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 = sinh" (((x ^2 ) - 1) / (2 * x)) ; :: thesis: verum