let x, y be Real; ( y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & x <> 0 implies x = (1 / 2) * (log (number_e,((y + 1) / (y - 1)))) )
A1:
0 < exp_R x
by SIN_COS:55;
set t = exp_R x;
assume that
A2:
y = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))
and
A3:
x <> 0
; x = (1 / 2) * (log (number_e,((y + 1) / (y - 1))))
y = ((exp_R x) + (1 / (exp_R x))) / ((exp_R x) - (exp_R (- x)))
by A2, 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) + (1 / (exp_R x))) / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x))
by A1, XCMPLX_1:127;
then
y = ((1 + ((exp_R x) * (exp_R x))) / (exp_R x)) / ((((exp_R x) ^2) - 1) / (exp_R x))
by A1, XCMPLX_1:113;
then A4:
y = (1 + ((exp_R x) ^2)) / (((exp_R x) ^2) - 1)
by A1, XCMPLX_1:55;
then
y * (((exp_R x) ^2) - 1) = 1 + ((exp_R x) ^2)
by A3, Th30, XCMPLX_1:87;
then A5:
(((exp_R x) ^2) * (y - 1)) / (y - 1) = (y + 1) / (y - 1)
;
exp_R x <> 1
by A3, Th29;
then A6:
( 1 < y or y < - 1 )
by A4, Lm12, SIN_COS:55;
then
( 1 - 1 < y - 1 or y - 1 < (- 1) - 1 )
by XREAL_1:14;
then
sqrt ((exp_R x) ^2) = sqrt ((y + 1) / (y - 1))
by A5, XCMPLX_1:89;
then A7:
exp_R x = sqrt ((y + 1) / (y - 1))
by A1, SQUARE_1:22;
A8:
0 < (y + 1) / (y - 1)
by A6, Lm7;
then
sqrt ((y + 1) / (y - 1)) = ((y + 1) / (y - 1)) to_power (1 / 2)
by ASYMPT_1:83;
then
log (number_e,(((y + 1) / (y - 1)) to_power (1 / 2))) = x
by A7, TAYLOR_1:12;
hence
x = (1 / 2) * (log (number_e,((y + 1) / (y - 1))))
by A8, Lm1, POWER:55, TAYLOR_1:11; verum