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 & 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)) )
let n be Element of NAT ; :: thesis: ( (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)) ) implies ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) )
assume A1: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q ) ; :: thesis: ( not (p ^2) - (4 * q) >= 0 or not p > 0 or not q > 0 or not n is even or not n >= 1 or ( 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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) )
assume that
A2: (p ^2) - (4 * q) >= 0 and
A3: p > 0 and
A4: q > 0 and
A5: ( n is even & n >= 1 ) ; :: 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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) )
- (- (4 * q)) > 0 by A4, XREAL_1:129;
then - (4 * q) < 0 ;
then (p ^2) + (- (4 * q)) < (p ^2) + 0 by XREAL_1:8;
then sqrt ((p ^2) - (4 * q)) < sqrt (p ^2) by A2, SQUARE_1:27;
then sqrt ((p ^2) - (4 * q)) < p by A3, SQUARE_1:22;
then - (sqrt ((p ^2) - (4 * q))) > - p by XREAL_1:24;
then (- (sqrt ((p ^2) - (4 * q)))) + p > ((- p) + 0) + p by XREAL_1:8;
then A6: ((0 + p) - (sqrt ((p ^2) - (4 * q)))) / 2 > 0 by XREAL_1:139;
A7: delta (1,(- p),q) = ((- p) ^2) - ((4 * 1) * q) by QUIN_1:def 1
.= (p ^2) - (4 * q) ;
then 0 <= sqrt (delta (1,(- p),q)) by A2, SQUARE_1:17, SQUARE_1:26;
then (- (- p)) + (sqrt (delta (1,(- p),q))) > 0 + 0 by A3;
then A8: ((0 + p) + (sqrt ((p ^2) - (4 * q)))) / 2 > 0 by A7, XREAL_1:139;

now :: 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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) )

per cases ( ( 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, A2, Th14;

suppose ( x |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) ; :: 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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) )

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) ) or ( 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)) ) or ( 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) ) or ( 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 A5, A8, A6, Th4; :: thesis: verum

end;

suppose ( x |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ; :: 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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) )

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) ) or ( 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)) ) or ( 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) ) or ( 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 A5, A8, A6, Th4; :: thesis: verum

end;

end;

end;

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) ) or ( 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)) ) or ( 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) ) or ( 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)) ) ) ; :: thesis: verum