let a, b, n be Nat; :: thesis: for c being Integer st c divides a - b holds
c divides (a |^ n) - (b |^ n)
let c be Integer; :: thesis: ( c divides a - b implies c divides (a |^ n) - (b |^ n) )
assume A1: c divides a - b ; :: thesis: c divides (a |^ n) - (b |^ n)
a - b divides (a |^ n) - (b |^ n) by NEWTON01:33;
hence c divides (a |^ n) - (b |^ n) by A1, INT_2:9; :: thesis: verum