let a, b, m be odd Nat; :: thesis: ( 4 divides (a |^ m) + (b |^ m) iff 4 divides a + b )
consider n being Nat such that
L0: m = (2 * n) + 1 by ABIAN:9;
( 4 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) implies 4 divides a + b )

proof

B2: 2 |^ 2 = 2 * 2 by NEWTON:81;
A1: 4 divides (a |^ (2 * n)) - (b |^ (2 * n)) by Th65;
A2: 4 divides ((a |^ (2 * n)) - (b |^ (2 * n))) * (((a |^ 1) - (b |^ 1)) / 2) by Th65, INT_2:2;
consider l being Nat such that
A3: ( l = ((a |^ (2 * n)) + (b |^ (2 * n))) / 2 & l is odd ) by A1, Th58, Lm63;
A4: (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) = ((((a |^ (2 * n)) + (b |^ (2 * n))) * ((a |^ 1) + (b |^ 1))) + (((a |^ (2 * n)) - (b |^ (2 * n))) * ((a |^ 1) - (b |^ 1)))) / 2 by NEWTON01:8
.= ((((a |^ (2 * n)) + (b |^ (2 * n))) * ((a |^ 1) + (b |^ 1))) / 2) + ((((a |^ (2 * n)) - (b |^ (2 * n))) * ((a |^ 1) - (b |^ 1))) / 2) ;
assume 4 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) ; :: thesis: 4 divides a + b
then 2 |^ 2 divides (((a |^ (2 * n)) + (b |^ (2 * n))) / 2) * ((a |^ 1) + (b |^ 1)) by B2, A2, A4, INT_2:1;
hence 4 divides a + b by B2, A3, Th67; :: thesis: verum

end;

hence ( 4 divides (a |^ m) + (b |^ m) iff 4 divides a + b ) by L0, Lm60; :: thesis: verum