let a, b be odd Nat; :: thesis: for m being even Nat holds 4 divides (a |^ m) - (b |^ m)
let m be even Nat; :: thesis: 4 divides (a |^ m) - (b |^ m)
consider n being Nat such that
L0: m = 2 * n by ABIAN:def 2;
L1: ( 4 divides a + b implies 4 divides (a |^ m) - (b |^ m) )
proof
assume A1: 4 divides a + b ; :: thesis: 4 divides (a |^ m) - (b |^ m)
a + b divides (a |^ m) - (b |^ m) by NEWTON01:36, L0;
hence 4 divides (a |^ m) - (b |^ m) by A1, INT_2:9; :: thesis: verum
end;
( 4 divides a - b implies 4 divides (a |^ m) - (b |^ m) ) by Th64;
hence 4 divides (a |^ m) - (b |^ m) by L1, Th58; :: thesis: verum