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:63;
assume A2: 0 < x ; :: thesis: log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x))
then 0 * 2 < x * 2 by XREAL_1:68;
then A3: 0 < (2 * x) ^2 by SQUARE_1:12;
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:76
.= 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:113
.= log (number_e,((((x ^2) - 1) / (2 * x)) + ((sqrt (((x ^2) + 1) ^2)) / (sqrt ((2 * x) ^2))))) by A2, SQUARE_1:30
.= log (number_e,((((x ^2) - 1) / (2 * x)) + (((x ^2) + 1) / (sqrt ((2 * x) ^2))))) by A1, SQUARE_1:22
.= log (number_e,((((x ^2) - 1) / (2 * x)) + (((x ^2) + 1) / (2 * x)))) by A2, SQUARE_1:22
.= 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:91
.= log (number_e,(x / (x / x))) by XCMPLX_1:77
.= 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