let x, y be Real; ( 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:55;
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:127;
then
y = ((((exp_R x) ^2) - 1) / (exp_R x)) / ((1 + ((exp_R x) * (exp_R x))) / (exp_R x))
by A1, XCMPLX_1:113;
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:87;
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:192;
y - 1 <> 0
by A2, Th31;
then
sqrt ((exp_R x) ^2) = sqrt ((y + 1) / (1 - y))
by A3, XCMPLX_1:89;
then A4:
exp_R x = sqrt ((y + 1) / (1 - y))
by A1, SQUARE_1:22;
- 1 < y
by A2, Lm11, SIN_COS:55;
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:83;
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:55, TAYLOR_1:11; verum