let a, b be odd Integer; :: thesis: for m being even Nat holds Parity ((a |^ m) + (b |^ m)) = 2
let m be even Nat; :: thesis: Parity ((a |^ m) + (b |^ m)) = 2
reconsider n = m / 2 as Nat ;
A1: ( (a |^ n) |^ 2 = a |^ (2 * n) & (b |^ n) |^ 2 = b |^ (2 * n) ) by NEWTON:9;
2 |^ (2 |-count (((a |^ n) |^ 2) + ((b |^ n) |^ 2))) = 2 |^ 1 by NEWTON03:74;
hence Parity ((a |^ m) + (b |^ m)) = 2 by A1, Def1; :: thesis: verum