let a, b, n be Nat; :: thesis: for p being prime Nat st not p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) & p divides (a |^ 2) - (b |^ 2) holds
p divides a - b
let p be prime Nat; :: thesis: ( not p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) & p divides (a |^ 2) - (b |^ 2) implies p divides a - b )
assume ( not p divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) & p divides (a |^ 2) - (b |^ 2) ) ; :: thesis: p divides a - b
then ( not p divides a + b & p divides (a + b) * (a - b) ) by NEWTON01:1, Th98;
hence p divides a - b by INT_5:7; :: thesis: verum