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))) )
assume A1: y = (1 / 2) * ((exp_R x) - (exp_R (- x))) ; :: thesis: x = log number_e ,(y + (sqrt ((y ^2 ) + 1)))
A2: exp_R x > 0 by SIN_COS:60;
A3: (2 * y) * (exp_R x) = ((exp_R x) - (1 / (exp_R x))) * (exp_R x) by A1, TAYLOR_1:4;
set t = exp_R x;
(2 * y) * (exp_R x) = ((exp_R x) * (exp_R x)) - ((1 / (exp_R x)) * (exp_R x)) by A3;
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 A2, XCMPLX_1:60;
then A4: ((1 * ((exp_R x) ^2 )) + ((- (2 * y)) * (exp_R x))) + (- 1) = 0 ;
A5: delta 1,(- (2 * y)),(- 1) = (((- 2) * y) ^2 ) - ((4 * 1) * (- 1)) by QUIN_1:def 1
.= (4 * (y ^2 )) + 4 ;
A6: 0 <= y ^2 by XREAL_1:65;
then A7: 0 + 1 <= (y ^2 ) + 1 by XREAL_1:8;
4 * 0 <= 4 * (y ^2 ) by A6;
then 0 + 4 <= (4 * (y ^2 )) + 4 by XREAL_1:8;
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 A4, A5, 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 A5, A7, 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 A7, SQUARE_1:85, SQUARE_1:97;
then A8: ( exp_R x = y + (sqrt ((y ^2 ) + 1)) or exp_R x = y - (sqrt ((y ^2 ) + 1)) ) ;
y < (sqrt ((y ^2 ) + 1)) + 0 by Lm10;
hence x = log number_e ,(y + (sqrt ((y ^2 ) + 1))) by A2, A8, TAYLOR_1:12, XREAL_1:21; :: thesis: verum