let x, y, p, q be Real; :: thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & 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) )
let n be Element of NAT ; :: thesis: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) implies ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) )
assume that
A1: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 ) and
A2: n is odd ; :: thesis: ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) )
( ( x |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) by A1, Th14;
hence ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) ) by A2, POWER:4; :: thesis: verum