let y, x be real number ; ( y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x))) implies x = (1 / 2) * (log number_e ,((1 + y) / (1 - y))) )
A1:
0 < exp_R x
by SIN_COS:60;
set t = exp_R x;
assume
y = ((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))
; x = (1 / 2) * (log number_e ,((1 + y) / (1 - y)))
then
y = ((exp_R x) - (1 / (exp_R x))) / ((exp_R x) + (exp_R (- x)))
by TAYLOR_1:4;
then
y = ((exp_R x) - (1 / (exp_R x))) / ((exp_R x) + (1 / (exp_R x)))
by TAYLOR_1:4;
then
y = ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) / ((exp_R x) + (1 / (exp_R x)))
by A1, XCMPLX_1:128;
then
y = ((((exp_R x) ^2 ) - 1) / (exp_R x)) / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x))
by A1, XCMPLX_1:114;
then A2:
y = (((exp_R x) ^2 ) - 1) / (1 + ((exp_R x) ^2 ))
by A1, XCMPLX_1:55;
then
(1 * y) + (((exp_R x) ^2 ) * y) = ((((exp_R x) ^2 ) - 1) / (1 + ((exp_R x) ^2 ))) * (1 + ((exp_R x) ^2 ))
;
then
(y + (((exp_R x) ^2 ) * y)) - (((exp_R x) ^2 ) - 1) = (((exp_R x) ^2 ) - 1) - (((exp_R x) ^2 ) - 1)
by A1, XCMPLX_1:88;
then
(((exp_R x) ^2 ) * (y - 1)) / (y - 1) = (- (y + 1)) / (y - 1)
;
then A3:
(((exp_R x) ^2 ) * (y - 1)) / (y - 1) = (y + 1) / (- (y - 1))
by XCMPLX_1:193;
y - 1 <> 0
by A2, Th31;
then
sqrt ((exp_R x) ^2 ) = sqrt ((y + 1) / (1 - y))
by A3, XCMPLX_1:90;
then A4:
exp_R x = sqrt ((y + 1) / (1 - y))
by A1, SQUARE_1:89;
- 1 < y
by A2, Lm11, SIN_COS:60;
then A5:
0 < (y + 1) / (1 - y)
by A2, Th31, Th32;
then
sqrt ((y + 1) / (1 - y)) = ((y + 1) / (1 - y)) to_power (1 / 2)
by ASYMPT_1:89;
then
log number_e ,(((y + 1) / (1 - y)) to_power (1 / 2)) = x
by A4, TAYLOR_1:12;
hence
x = (1 / 2) * (log number_e ,((1 + y) / (1 - y)))
by A5, Lm1, POWER:63, TAYLOR_1:11; verum