let x, y be Real; :: thesis: ( y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 & not x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) implies x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) )
A1: 0 < exp_R x by SIN_COS:55;
set t = exp_R x;
assume that
A2: y = 1 / (((exp_R x) - (exp_R (- x))) / 2) and
A3: x <> 0 ; :: thesis: ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) )
A4: delta (y,(- 2),(- y)) = ((- 2) ^2) - ((4 * y) * (- y)) by QUIN_1:def 1
.= 4 + (4 * (y ^2)) ;
y = (1 * 2) / (2 * (((exp_R x) - (exp_R (- x))) / 2)) by A2, XCMPLX_1:91;
then y = 2 / ((exp_R x) - (1 / (exp_R x))) by TAYLOR_1:4;
then y = 2 / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by A1, XCMPLX_1:127;
then A5: y = 2 * ((exp_R x) / (((exp_R x) ^2) - 1)) by XCMPLX_1:79;
then A6: y = (2 * (exp_R x)) / (((exp_R x) ^2) - 1) ;
then y * (((exp_R x) ^2) - 1) = 2 * (exp_R x) by A3, Th30, XCMPLX_1:87;
then A7: ((y * ((exp_R x) ^2)) + ((- 2) * (exp_R x))) + (- y) = 0 ;
A8: exp_R x <> 1 by A3, Th29;
then A9: (2 * (exp_R x)) / (((exp_R x) ^2) - 1) <> 0 by Lm20, SIN_COS:55;