let x be Real; ( 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
; log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x))
then
0 * 2 < x * 2
;
then A3:
0 < (2 * x) ^2
;
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))
; verum