let x, y be Real; :: thesis: ( 1 <= x & 1 <= y & |.y.| <= |.x.| implies (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) )
assume that
A1: 1 <= x and
A2: 1 <= y and
A3: |.y.| <= |.x.| ; :: thesis: (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1))))
A4: ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23;
A5: 0 <= (y ^2) - 1 by A2, Lm3;
set t = (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)));
A6: y - (sqrt ((y ^2) - 1)) > 0 by A2, Th25;
A7: 0 <= (x ^2) - 1 by A1, Lm3;
A8: cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) = - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1)))))
.= - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) - ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1))))) by A7, A5, SQUARE_1:def 2
.= - (log (number_e,(((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))))))) ;
A9: (cosh2" x) - (cosh2" y) = - ((log (number_e,(x + (sqrt ((x ^2) - 1))))) - (log (number_e,(y + (sqrt ((y ^2) - 1))))))
.= - (log (number_e,((x + (sqrt ((x ^2) - 1))) / (y + (sqrt ((y ^2) - 1)))))) by A4, Lm1, POWER:54, TAYLOR_1:11
.= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y + (sqrt ((y ^2) - 1))) * (y - (sqrt ((y ^2) - 1))))))) by A6, XCMPLX_1:91
.= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((sqrt ((y ^2) - 1)) ^2)))))
.= - (log (number_e,(((x + (sqrt ((x ^2) - 1))) * (y - (sqrt ((y ^2) - 1)))) / ((y ^2) - ((y ^2) - 1))))) by A5, SQUARE_1:def 2
.= - (log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1))))))
.= - (log (number_e,((((x * y) - (x * (sqrt ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))))) by A7, A5, SQUARE_1:29
.= - (log (number_e,((((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (y * (sqrt ((x ^2) - 1)))) - (x * (sqrt ((y ^2) - 1)))))) ;
(y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1))) = sqrt (((y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))) ^2) by A1, A2, A3, Th26, SQUARE_1:22
.= sqrt ((((y ^2) * ((sqrt ((x ^2) - 1)) ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2))
.= sqrt ((((y ^2) * ((x ^2) - 1)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x * (sqrt ((y ^2) - 1))) ^2)) by A7, SQUARE_1:def 2
.= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((sqrt ((y ^2) - 1)) ^2)))
.= sqrt (((((x * y) ^2) - (y ^2)) - ((2 * (y * (sqrt ((x ^2) - 1)))) * (x * (sqrt ((y ^2) - 1))))) + ((x ^2) * ((y ^2) - 1))) by A5, SQUARE_1:def 2
.= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))))
.= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) - (((2 * x) * y) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) by A7, A5, SQUARE_1:29 ;
hence (cosh2" x) - (cosh2" y) = cosh2" ((x * y) - (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A9, A8; :: thesis: verum