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)
proof
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;
hence ( a is odd & b is odd & m is even implies (a |^ m) + (b |^ m) <> c |^ m ) ; :: thesis: verum