let y, x be real number ; ( 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:92;
then
( 0 < exp_R x & y = 2 / ((exp_R x) + (1 / (exp_R x))) )
by SIN_COS:60, TAYLOR_1:4;
then
y = 2 / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x))
by XCMPLX_1:114;
then
y = 2 * ((exp_R x) / (1 + ((exp_R x) ^2 )))
by XCMPLX_1:80;
then A2:
y = (2 * (exp_R x)) / (1 + ((exp_R x) ^2 ))
;
then A3:
0 < y
by Lm13, SIN_COS:60;
1 + ((exp_R x) ^2 ) > 0
by Lm6;
then A4:
y * (1 + ((exp_R x) ^2 )) = 2 * (exp_R x)
by A2, XCMPLX_1:88;
A5:
y <= 1
by A2, Lm14, SIN_COS:60;
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: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 A7:
( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = (1 - (sqrt (1 - (y ^2 )))) / y )
by XCMPLX_1:92;
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: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 A8:
( exp_R x = (1 + (sqrt (1 - (y ^2 )))) / y or exp_R x = y / (1 + (sqrt (1 - (y ^2 )))) )
by A3, XCMPLX_1:92;
( 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:63, 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