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

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