let k be Nat; :: thesis: for n being prime Nat
for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k)
let n be prime Nat; :: thesis: for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k)
let a, b be positive Nat; :: thesis: (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k)
((a + b) |^ n) - ((a |^ n) + (b |^ n)) divides (((a + b) |^ n) |^ k) - (((a |^ n) + (b |^ n)) |^ k) by NEWTON01:33;
then A1: ((a + b) |^ n) - ((a |^ n) + (b |^ n)) divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k) by NEWTON:9;
(n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n)) by Th55;
hence (n * a) * b divides ((a + b) |^ (k * n)) - (((a |^ n) + (b |^ n)) |^ k) by A1, INT_2:9; :: thesis: verum