theorem :: POLYEQ_4:16

for x, y, p, q being Real
for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & p > 0 & q > 0 & n is even & n >= 1 & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) holds
( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) )