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 & not n is even & 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 & not n is even & 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: not n is even ; :: 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:5; :: thesis: verum