let y, x be real number ; :: 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:60;
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:65;
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:97;
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:85, SQUARE_1:97;
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:21; :: thesis: verum