let a, b, c, m be Nat; :: thesis: ( a is odd & b is odd & m is even implies (a |^ m) + (b |^ m) <> c |^ m )

for n being Nat st a is odd & b is odd holds

(a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n)

for n being Nat st a is odd & b is odd holds

(a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n)

proof

hence
( a is odd & b is odd & m is even implies (a |^ m) + (b |^ m) <> c |^ m )
; :: thesis: verum
let n be Nat; :: thesis: ( a is odd & b is odd implies (a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n) )

A1: ( a |^ (2 * n) = (a |^ n) |^ 2 & b |^ (2 * n) = (b |^ n) |^ 2 & c |^ (2 * n) = (c |^ n) |^ 2 ) by NEWTON:9;

assume ( a is odd & b is odd ) ; :: thesis: (a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n)

hence (a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n) by A1, Lm40; :: thesis: verum

end;A1: ( a |^ (2 * n) = (a |^ n) |^ 2 & b |^ (2 * n) = (b |^ n) |^ 2 & c |^ (2 * n) = (c |^ n) |^ 2 ) by NEWTON:9;

assume ( a is odd & b is odd ) ; :: thesis: (a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n)

hence (a |^ (2 * n)) + (b |^ (2 * n)) <> c |^ (2 * n) by A1, Lm40; :: thesis: verum