let x, y be Real; ( y = (1 / 2) * ((exp_R x) - (exp_R (- x))) implies x = log (number_e,(y + (sqrt ((y ^2) + 1)))) )
A1:
exp_R x > 0
by SIN_COS:55;
set t = exp_R x;
A2: delta (1,(- (2 * y)),(- 1)) =
(((- 2) * y) ^2) - ((4 * 1) * (- 1))
by QUIN_1:def 1
.=
(4 * (y ^2)) + 4
;
A3:
0 <= y ^2
by XREAL_1:63;
assume
y = (1 / 2) * ((exp_R x) - (exp_R (- x)))
; x = log (number_e,(y + (sqrt ((y ^2) + 1))))
then
(2 * y) * (exp_R x) = ((exp_R x) - (1 / (exp_R x))) * (exp_R x)
by TAYLOR_1:4;
then
(2 * y) * (exp_R x) = ((exp_R x) ^2) - (((exp_R x) * 1) / (exp_R x))
;
then
((2 * y) * (exp_R x)) - ((2 * y) * (exp_R x)) = (((exp_R x) ^2) - 1) - ((2 * y) * (exp_R x))
by A1, XCMPLX_1:60;
then
((1 * ((exp_R x) ^2)) + ((- (2 * y)) * (exp_R x))) + (- 1) = 0
;
then
( exp_R x = ((- (- (2 * y))) + (sqrt (delta (1,(- (2 * y)),(- 1))))) / (2 * 1) or exp_R x = ((- (- (2 * y))) - (sqrt (delta (1,(- (2 * y)),(- 1))))) / (2 * 1) )
by A2, A3, QUIN_1:15;
then
( exp_R x = ((2 * y) + ((sqrt 4) * (sqrt ((y ^2) + 1)))) / 2 or exp_R x = ((2 * y) - (sqrt (4 * ((y ^2) + 1)))) / 2 )
by A2, A3, SQUARE_1:29;
then
( exp_R x = ((2 * y) + (2 * (sqrt ((y ^2) + 1)))) / 2 or exp_R x = ((2 * y) - (2 * (sqrt ((y ^2) + 1)))) / 2 )
by A3, SQUARE_1:20, SQUARE_1:29;
then A4:
( exp_R x = y + (sqrt ((y ^2) + 1)) or exp_R x = y - (sqrt ((y ^2) + 1)) )
;
y < (sqrt ((y ^2) + 1)) + 0
by Lm8;
hence
x = log (number_e,(y + (sqrt ((y ^2) + 1))))
by A1, A4, TAYLOR_1:12, XREAL_1:19; verum