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 odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) 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 odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) 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 odd and

A4: a * b <> 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )

consider m being Nat such that

A5: n = (2 * m) + 1 by A3, ABIAN:9;

A6: n > 0 by A5;

( 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 odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) 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 odd and

A4: a * b <> 0 ; :: thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )

consider m being Nat such that

A5: n = (2 * m) + 1 by A3, ABIAN:9;

A6: n > 0 by A5;

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

hence
( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) )
; :: thesis: verumper cases
( x = 0 or y = 0 )
by A2;

end;

suppose A7:
x = 0
; :: thesis: ( ( x = 0 & y = n -root (p / b) ) 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 A6, POWER:def 2;

then y |^ n = p / b by A4, XCMPLX_1:89;

hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A7, POWER:4; :: thesis: verum

end;then (a * 0) + (b * (y |^ n)) = p by A6, POWER:def 2;

then y |^ n = p / b by A4, XCMPLX_1:89;

hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A7, POWER:4; :: thesis: verum

suppose A8:
y = 0
; :: thesis: ( ( x = 0 & y = n -root (p / b) ) 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 A6, POWER:def 2;

then x |^ n = p / a by A4, XCMPLX_1:89;

hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A8, POWER:4; :: thesis: verum

end;then (a * (x |^ n)) + (b * 0) = p by A6, POWER:def 2;

then x |^ n = p / a by A4, XCMPLX_1:89;

hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A8, POWER:4; :: thesis: verum