let x, y, a, b be Real; :: thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) holds
( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) )
let n be Element of NAT ; :: thesis: ( (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) implies ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) )
assume A1: ( (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b ) ; :: thesis: ( not n is even or not n >= 1 or not a + b > 0 or not a - b > 0 or ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) )
assume that
A2: ( n is even & n >= 1 ) and
A3: ( a + b > 0 & a - b > 0 ) ; :: thesis: ( ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) )
( (a + b) / 2 > 0 & (a - b) / 2 > 0 ) by A3, XREAL_1:139;
hence ( ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) ) by A1, A2, Th4; :: thesis: verum