let x, y be real number ; (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) - (y * (sqrt (1 + (x ^2 )))))
set t = ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y);
set q = sqrt ((((x * (sqrt (1 + (y ^2 )))) - (y * (sqrt (1 + (x ^2 ))))) ^2 ) + 1);
A1:
(x ^2 ) + 1 >= 0
by Lm6;
y + 0 < sqrt ((y ^2 ) + 1)
by Lm8;
then A2:
(sqrt ((y ^2 ) + 1)) - y > 0
by XREAL_1:22;
A3:
(y ^2 ) + 1 >= 0
by Lm6;
((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) >= 0
by Lm9;
then A4: ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y) =
sqrt ((((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) - (x * y)) ^2 )
by SQUARE_1:89
.=
sqrt (((((sqrt ((x ^2 ) + 1)) ^2 ) * ((sqrt ((y ^2 ) + 1)) ^2 )) - ((2 * ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) * (x * y))) + ((x * y) ^2 ))
.=
sqrt (((((x ^2 ) + 1) * ((sqrt ((y ^2 ) + 1)) ^2 )) - ((2 * ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) * (x * y))) + ((x * y) ^2 ))
by A1, SQUARE_1:def 4
.=
sqrt (((((x ^2 ) + 1) * ((y ^2 ) + 1)) - ((2 * ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) * (x * y))) + ((x * y) ^2 ))
by A3, SQUARE_1:def 4
.=
sqrt (((((2 * ((x * y) ^2 )) + (x ^2 )) + (y ^2 )) + 1) - ((2 * (x * y)) * ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))))
;
A5: sqrt ((((x * (sqrt (1 + (y ^2 )))) - (y * (sqrt (1 + (x ^2 ))))) ^2 ) + 1) =
sqrt (((((x ^2 ) * ((sqrt (1 + (y ^2 ))) ^2 )) - ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y * (sqrt (1 + (x ^2 )))) ^2 )) + 1)
.=
sqrt (((((x ^2 ) * (1 + (y ^2 ))) - ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y * (sqrt (1 + (x ^2 )))) ^2 )) + 1)
by A3, SQUARE_1:def 4
.=
sqrt (((((x ^2 ) + ((x ^2 ) * (y ^2 ))) - ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y ^2 ) * ((sqrt (1 + (x ^2 ))) ^2 ))) + 1)
.=
sqrt (((((x ^2 ) + ((x ^2 ) * (y ^2 ))) - ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y ^2 ) * (1 + (x ^2 )))) + 1)
by A1, SQUARE_1:def 4
.=
sqrt (((((x ^2 ) + (y ^2 )) + (2 * ((x * y) ^2 ))) + 1) - ((((2 * x) * y) * (sqrt (1 + (y ^2 )))) * (sqrt (1 + (x ^2 )))))
;
( (sqrt ((x ^2 ) + 1)) + x > 0 & (sqrt ((y ^2 ) + 1)) + y > 0 )
by Th5;
then (sinh" x) - (sinh" y) =
log number_e ,((x + (sqrt ((x ^2 ) + 1))) / (y + (sqrt ((y ^2 ) + 1))))
by Lm1, POWER:62, TAYLOR_1:11
.=
log number_e ,(((x + (sqrt ((x ^2 ) + 1))) * ((sqrt ((y ^2 ) + 1)) - y)) / ((y + (sqrt ((y ^2 ) + 1))) * ((sqrt ((y ^2 ) + 1)) - y)))
by A2, XCMPLX_1:92
.=
log number_e ,(((x + (sqrt ((x ^2 ) + 1))) * ((sqrt ((y ^2 ) + 1)) - y)) / (((sqrt ((y ^2 ) + 1)) ^2 ) - (y ^2 )))
.=
log number_e ,(((x + (sqrt ((x ^2 ) + 1))) * ((sqrt ((y ^2 ) + 1)) - y)) / (((y ^2 ) + 1) - (y ^2 )))
by A3, SQUARE_1:def 4
.=
log number_e ,((((x * (sqrt ((y ^2 ) + 1))) - (y * (sqrt ((x ^2 ) + 1)))) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) - (x * y))
;
hence
(sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) - (y * (sqrt (1 + (x ^2 )))))
by A4, A5; verum