let x, y be Real; ( 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))) )
set t = exp_R x;
A1: delta (y,(- 2),y) =
((- 2) ^2) - ((4 * y) * y)
by QUIN_1:def 1
.=
4 - (4 * (y ^2))
;
assume
y = 1 / (((exp_R x) + (exp_R (- x))) / 2)
; ( 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:91;
then
( 0 < exp_R x & y = 2 / ((exp_R x) + (1 / (exp_R x))) )
by SIN_COS:55, TAYLOR_1:4;
then
y = 2 / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x))
by XCMPLX_1:113;
then
y = 2 * ((exp_R x) / (1 + ((exp_R x) ^2)))
by XCMPLX_1:79;
then A2:
y = (2 * (exp_R x)) / (1 + ((exp_R x) ^2))
;
then A3:
0 < y
by Lm13, SIN_COS:55;
1 + ((exp_R x) ^2) > 0
by Lm6;
then A4:
y * (1 + ((exp_R x) ^2)) = 2 * (exp_R x)
by A2, XCMPLX_1:87;
A5:
y <= 1
by A2, Lm14, SIN_COS:55;
then A6:
0 <= 1 - (y ^2)
by A3, Lm16;
Polynom (y,(- 2),y,(exp_R x)) = ((y * ((exp_R x) ^2)) + ((- 2) * (exp_R x))) + y
by POLYEQ_1:def 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 A3, A5, A4, A1, Lm17, 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 A1;
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:20, SQUARE_1:29;
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 A7:
( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = (1 - (sqrt (1 - (y ^2)))) / y )
by XCMPLX_1:91;
0 < 1 + (sqrt (1 - (y ^2)))
by A3, A5, Lm18;
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 A7, XCMPLX_1:91;
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 2;
then A8:
( exp_R x = (1 + (sqrt (1 - (y ^2)))) / y or exp_R x = y / (1 + (sqrt (1 - (y ^2)))) )
by A3, XCMPLX_1:91;
( log (number_e,(exp_R x)) = x & 1 / ((1 + (sqrt (1 - (y ^2)))) / y) = ((1 + (sqrt (1 - (y ^2)))) / y) to_power (- 1) )
by A3, A5, Lm19, Th1, TAYLOR_1:12;
then A9:
( 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 A8, XCMPLX_1:57;
0 < (1 + (sqrt (1 - (y ^2)))) / y
by A3, A5, Lm19;
then
( log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) = x or (- 1) * (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) = x )
by A9, Lm1, POWER:55, TAYLOR_1:11;
hence
( x = log (number_e,((1 + (sqrt (1 - (y ^2)))) / y)) or x = - (log (number_e,((1 + (sqrt (1 - (y ^2)))) / y))) )
; verum