let x, y be Real; :: thesis: ( 1 <= x & 1 <= y implies (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) )
assume that
A1: 1 <= x and
A2: 1 <= y ; :: thesis: (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1))))
A3: (y ^2) - 1 >= 0 by A2, Lm3;
A4: ( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) ) by A1, A2, Th23;
set t = (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)));
A5: (x ^2) - 1 >= 0 by A1, Lm3;
(x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) = sqrt (((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) ^2) by A1, A2, Th24, SQUARE_1:22
.= sqrt ((((x ^2) * ((sqrt ((y ^2) - 1)) ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2))
.= sqrt ((((x ^2) * ((y ^2) - 1)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2)) by A3, SQUARE_1:def 2
.= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((sqrt ((x ^2) - 1)) ^2)))
.= sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((x ^2) - 1))) by A5, SQUARE_1:def 2
.= sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) ;
then A6: - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) = - (log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * ((sqrt ((y ^2) - 1)) * (sqrt ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))))
.= - (log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) by A5, A3, SQUARE_1:29 ;
A7: 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 A5, A3, SQUARE_1:def 2
.= - (log (number_e,((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) + (x * y))))) ;
(cosh2" x) + (cosh2" y) = (- 1) * ((log (number_e,(x + (sqrt ((x ^2) - 1))))) + (log (number_e,(y + (sqrt ((y ^2) - 1))))))
.= (- 1) * (log (number_e,((x + (sqrt ((x ^2) - 1))) * (y + (sqrt ((y ^2) - 1)))))) by A4, Lm1, POWER:53, TAYLOR_1:11
.= - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))) + (x * y))))
.= - (log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))) by A5, A3, SQUARE_1:29 ;
hence (cosh2" x) + (cosh2" y) = cosh2" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) by A6, A7; :: thesis: verum