let x be real number ; sinh" x = tanh" (x / (sqrt ((x ^2) + 1)))
set t = (sqrt ((x ^2) + 1)) + x;
A1:
(sqrt ((x ^2) + 1)) + x > 0
by Th5;
A2:
(x ^2) + 1 > 0
by Lm6;
A3:
sqrt ((x ^2) + 1) > 0
by Th4;
then tanh" (x / (sqrt ((x ^2) + 1))) =
(1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (1 - (x / (sqrt ((x ^2) + 1)))))))
by XCMPLX_1:114
.=
(1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (((1 * (sqrt ((x ^2) + 1))) - x) / (sqrt ((x ^2) + 1))))))
by A3, XCMPLX_1:128
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) / ((sqrt ((x ^2) + 1)) - x))))
by A3, XCMPLX_1:55
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) - x) * ((sqrt ((x ^2) + 1)) + x)))))
by A1, XCMPLX_1:92
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) * (sqrt ((x ^2) + 1))) - (x ^2)))))
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / ((sqrt (((x ^2) + 1) ^2)) - (x ^2)))))
by A2, SQUARE_1:97
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((x ^2) + 1) - (x ^2)))))
by A2, SQUARE_1:89
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) ^2)))
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) to_power 2)))
by POWER:53
.=
(1 / 2) * (2 * (log (number_e,((sqrt ((x ^2) + 1)) + x))))
by A1, Lm1, POWER:63, TAYLOR_1:11
.=
log (number_e,((sqrt ((x ^2) + 1)) + x))
;
hence
sinh" x = tanh" (x / (sqrt ((x ^2) + 1)))
; verum