let x be real number ; ( x ^2 < 1 implies tanh" x = sinh" (x / (sqrt (1 - (x ^2 )))) )
assume A1:
x ^2 < 1
; tanh" x = sinh" (x / (sqrt (1 - (x ^2 ))))
then A2:
x + 1 > 0
by Th11;
A3:
sqrt (x + 1) > 0
by A1, Th11, SQUARE_1:93;
A4:
(x + 1) / (1 - x) > 0
by A1, Lm4;
A5:
1 - (x ^2 ) > 0
by A1, XREAL_1:52;
A6:
1 - x > 0
by A1, Th11;
then A7:
sqrt ((x + 1) / (1 - x)) = ((x + 1) / (1 - x)) to_power (1 / 2)
by A2, ASYMPT_1:89;
sinh" (x / (sqrt (1 - (x ^2 )))) =
log number_e ,((x / (sqrt (1 - (x ^2 )))) + (sqrt (((x ^2 ) / ((sqrt (1 - (x ^2 ))) ^2 )) + 1)))
by XCMPLX_1:77
.=
log number_e ,((x / (sqrt (1 - (x ^2 )))) + (sqrt (((x ^2 ) / (1 - (x ^2 ))) + 1)))
by A5, SQUARE_1:def 4
.=
log number_e ,((x / (sqrt (1 - (x ^2 )))) + (sqrt (((x ^2 ) + ((1 - (x ^2 )) * 1)) / (1 - (x ^2 )))))
by A5, XCMPLX_1:114
.=
log number_e ,((x / (sqrt (1 - (x ^2 )))) + ((sqrt 1) / (sqrt (1 - (x ^2 )))))
by A5, SQUARE_1:99
.=
log number_e ,((x + 1) / (sqrt ((1 - x) * (1 + x))))
by SQUARE_1:83
.=
log number_e ,((sqrt ((x + 1) ^2 )) / (sqrt ((1 - x) * (1 + x))))
by A2, SQUARE_1:89
.=
log number_e ,(((sqrt (x + 1)) * (sqrt (x + 1))) / (sqrt ((1 - x) * (1 + x))))
by A2, SQUARE_1:97
.=
log number_e ,(((sqrt (x + 1)) * (sqrt (x + 1))) / ((sqrt (1 - x)) * (sqrt (1 + x))))
by A2, A6, SQUARE_1:97
.=
log number_e ,((sqrt (x + 1)) / (sqrt (1 - x)))
by A3, XCMPLX_1:92
.=
log number_e ,(sqrt ((x + 1) / (1 - x)))
by A2, A6, SQUARE_1:99
.=
(1 / 2) * (log number_e ,((1 + x) / (1 - x)))
by A4, A7, Lm1, POWER:63, TAYLOR_1:11
;
hence
tanh" x = sinh" (x / (sqrt (1 - (x ^2 ))))
; verum