theorem :: NEWTON02:162

for a, b being Nat
for n being prime Nat holds
( n divides (a |^ n) + (b |^ n) iff n divides (a + b) |^ n ) by Th60, Th62;