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