let y, x be real number ; :: 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:60;
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: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 A6, SQUARE_1:85, SQUARE_1:97;
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:90;
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 4;
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:63, 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