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