let a, b, m be odd Nat; :: thesis: ( 4 divides a + b implies 4 divides (a |^ m) + (b |^ m) )
consider n being Nat such that
A0: m = (2 * n) + 1 by ABIAN:9;
assume A1: 4 divides a + b ; :: thesis: 4 divides (a |^ m) + (b |^ m)
a + b divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) by NEWTON01:35;
hence 4 divides (a |^ m) + (b |^ m) by A0, A1, INT_2:9; :: thesis: verum