let a, b, n be Nat; :: thesis: for p being prime Nat st p divides a + b holds
p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1))
let p be prime Nat; :: thesis: ( p divides a + b implies p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) )
A1: a + b divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) by NEWTON01:35;
assume p divides a + b ; :: thesis: p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1))
hence p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) by A1, INT_2:9; :: thesis: verum