let x, y be Real; :: thesis: ( y = (1 / 2) * ((exp_R x) + (exp_R (- x))) & 1 <= y & not x = log (number_e,(y + (sqrt ((y ^2) - 1)))) implies x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) )
assume that
A1: y = (1 / 2) * ((exp_R x) + (exp_R (- x))) and
A2: 1 <= y ; :: thesis: ( x = log (number_e,(y + (sqrt ((y ^2) - 1)))) or x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) )
A3: y + (sqrt ((y ^2) - 1)) > 0 by A2, Lm10;
set t = exp_R x;
(2 * y) * (exp_R x) = ((exp_R x) + (1 / (exp_R x))) * (exp_R x) by A1, TAYLOR_1:4;
then ( 0 < exp_R x & (2 * y) * (exp_R x) = ((exp_R x) ^2) + (((exp_R x) * 1) / (exp_R x)) ) by SIN_COS:55;
then ((2 * y) * (exp_R x)) - ((2 * y) * (exp_R x)) = (((exp_R x) ^2) + 1) - ((2 * y) * (exp_R x)) by XCMPLX_1:60;
then A4: 0 = ((1 * ((exp_R x) ^2)) + ((- (2 * y)) * (exp_R x))) + 1 ;
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) - 1 by A2, Lm3;
then 0 * 4 <= ((y ^2) - 1) * 4 ;
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 A6, A5, 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 A6, SQUARE_1:20, SQUARE_1:29;
then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(y - (sqrt ((y ^2) - 1)))) = x ) by TAYLOR_1:12;
then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y - (sqrt ((y ^2) - 1))) * (y + (sqrt ((y ^2) - 1)))) / (y + (sqrt ((y ^2) - 1))))) = x ) by A3, XCMPLX_1:89;
then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y ^2) - ((sqrt ((y ^2) - 1)) ^2)) / (y + (sqrt ((y ^2) - 1))))) = x ) ;
then A7: ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or log (number_e,(((y ^2) - ((y ^2) - 1)) / (y + (sqrt ((y ^2) - 1))))) = x ) by A6, SQUARE_1:def 2;
1 / (y + (sqrt ((y ^2) - 1))) = (y + (sqrt ((y ^2) - 1))) to_power (- 1) by A3, Th1;
then ( log (number_e,(y + (sqrt ((y ^2) - 1)))) = x or (- 1) * (log (number_e,(y + (sqrt ((y ^2) - 1))))) = x ) by A3, A7, Lm1, POWER:55, TAYLOR_1:11;
hence ( x = log (number_e,(y + (sqrt ((y ^2) - 1)))) or x = - (log (number_e,(y + (sqrt ((y ^2) - 1))))) ) ; :: thesis: verum