theorem :: NEWTON02:94

for a, b, c being Nat
for n being odd Nat holds
( 3 divides (a + b) - c iff 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) )