let x, y, a, b, p be Real; :: thesis: for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) holds
( x = - (n -root (p / a)) & y = 0 )
let n be Element of NAT ; :: thesis: ( (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) implies ( x = - (n -root (p / a)) & y = 0 ) )
assume that
A1: (a * (x |^ n)) + (b * (y |^ n)) = p and
A2: x * y = 0 and
A3: ( n is even & n >= 1 ) and
A4: p / b > 0 and
A5: p / a > 0 and
A6: a * b <> 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) )
n >= 1 by A3;
then A7: n > 0 ;

per cases ( x = 0 or y = 0 ) by A2;

suppose A8: x = 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) )

then (a * (0 to_power n)) + (b * (y |^ n)) = p by A1;
then (a * 0) + (b * (y |^ n)) = p by A7, POWER:def 2;
then y |^ n = p / b by A6, XCMPLX_1:89;
hence ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) by A3, A4, A8, Th4; :: thesis: verum

end;

suppose A9: y = 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) )

then (a * (x |^ n)) + (b * (0 to_power n)) = p by A1;
then (a * (x |^ n)) + (b * 0) = p by A7, POWER:def 2;
then x |^ n = p / a by A6, XCMPLX_1:89;
hence ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) by A3, A5, A9, Th4; :: thesis: verum

end;

end;