let y, x be real number ; :: thesis: ( not y = 1 / (((exp_R x) + (exp_R (- x))) / 2) or x = log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) or x = - (log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y)) )
A1: 0 < exp_R x by SIN_COS:60;
A2: log number_e ,(exp_R x) = x by TAYLOR_1:12;
assume y = 1 / (((exp_R x) + (exp_R (- x))) / 2) ; :: thesis: ( x = log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) or x = - (log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y)) )
then y = (1 * 2) / (2 * (((exp_R x) + (exp_R (- x))) / 2)) by XCMPLX_1:92;
then y = 2 / ((exp_R x) + (1 / (exp_R x))) by TAYLOR_1:4;
then y = 2 / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x)) by A1, XCMPLX_1:114;
then A3: y = 2 * ((exp_R x) / (1 + ((exp_R x) ^2 ))) by XCMPLX_1:80;
set t = exp_R x;
A4: y = (2 * (exp_R x)) / (1 + ((exp_R x) ^2 )) by A3;
then A5: ( 0 < y & y <= 1 ) by A1, Lm15, Lm16;
then A6: ( 0 <= 1 - (y ^2 ) & 0 <= 4 - (4 * (y ^2 )) & 0 < 1 + (sqrt (1 - (y ^2 ))) & 0 < (1 + (sqrt (1 - (y ^2 )))) / y ) by Lm19, Lm20, Lm21, Lm22;
then A7: 1 / ((1 + (sqrt (1 - (y ^2 )))) / y) = ((1 + (sqrt (1 - (y ^2 )))) / y) to_power (- 1) by Th1;
1 + ((exp_R x) ^2 ) > 0 by Lm8;
then A8: y * (1 + ((exp_R x) ^2 )) = 2 * (exp_R x) by A4, XCMPLX_1:88;
A9: Polynom y,(- 2),y,(exp_R x) = ((y * ((exp_R x) ^2 )) + ((- 2) * (exp_R x))) + y by POLYEQ_1:def 2;
A10: delta y,(- 2),y = ((- 2) ^2 ) - ((4 * y) * y) by QUIN_1:def 1
.= 4 - (4 * (y ^2 )) ;
then ( exp_R x = ((- (- 2)) + (sqrt (delta y,(- 2),y))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta y,(- 2),y))) / (2 * y) ) by A5, A6, A8, A9, QUIN_1:15;
then ( exp_R x = (2 + (sqrt (4 * (1 - (y ^2 ))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 - (y ^2 ))))) / (2 * y) ) by A10;
then ( exp_R x = (2 + (2 * (sqrt (1 - (y ^2 ))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 - (y ^2 ))))) / (2 * y) ) by A6, SQUARE_1:85, SQUARE_1:97;
then ( exp_R x = (2 * (1 + (sqrt (1 - (y ^2 ))))) / (2 * y) or exp_R x = (2 * (1 - (sqrt (1 - (y ^2 ))))) / (2 * y) ) ;
then ( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = (1 - (sqrt (1 - (y ^2 )))) / y ) by XCMPLX_1:92;
then ( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = ((1 - (sqrt (1 - (y ^2 )))) * (1 + (sqrt (1 - (y ^2 ))))) / (y * (1 + (sqrt (1 - (y ^2 ))))) ) by A6, XCMPLX_1:92;
then ( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = (1 - ((sqrt (1 - (y ^2 ))) ^2 )) / (y * (1 + (sqrt (1 - (y ^2 ))))) ) ;
then ( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = (1 - (1 - (y ^2 ))) / (y * (1 + (sqrt (1 - (y ^2 ))))) ) by A6, SQUARE_1:def 4;
then ( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = y / (1 + (sqrt (1 - (y ^2 )))) ) by A5, XCMPLX_1:92;
then ( log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) = x or log number_e ,(((1 + (sqrt (1 - (y ^2 )))) / y) to_power (- 1)) = x ) by A2, A7, XCMPLX_1:57;
then ( log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) = x or (- 1) * (log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y)) = x ) by A6, Lm2, POWER:63;
hence ( x = log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y) or x = - (log number_e ,((1 + (sqrt (1 - (y ^2 )))) / y)) ) ; :: thesis: verum