let n be prime Nat; :: thesis: for a, b being positive Nat holds (n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n))
let a, b be positive Nat; :: thesis: (n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n))
reconsider g = (a,b) In_Power n as FinSequence of NAT by Th1;
reconsider h = (((a,b) In_Power n) | n) /^ 1 as FinSequence of NAT by Th1;
A1: for k being Nat st k in dom h holds
(n * a) * b divides h . k by Th54;
Sum g = ((a |^ n) + (b |^ n)) + (Sum h) by Th48;
then (a + b) |^ n = ((Sum h) + (a |^ n)) + (b |^ n) by NEWTON:30;
hence (n * a) * b divides ((a + b) |^ n) - ((a |^ n) + (b |^ n)) by A1, INT_4:36; :: thesis: verum