let x, y be Real; :: thesis: ( 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))) ; :: thesis: 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; :: thesis: verum