let n be prime Nat; :: thesis: n divides (2 |^ n) - 2

reconsider h = Newton_Coeff n as FinSequence of NAT by Th1;

reconsider f = ((Newton_Coeff n) | n) /^ 1 as FinSequence of NAT by Th1;

A2: for k being Nat st k in dom f holds

n divides f . k by Th39;

Sum h = (Sum f) + 2 by Th35;

then 2 |^ n = (Sum f) + 2 by NEWTON:32;

hence n divides (2 |^ n) - 2 by A2, INT_4:36; :: thesis: verum

reconsider h = Newton_Coeff n as FinSequence of NAT by Th1;

reconsider f = ((Newton_Coeff n) | n) /^ 1 as FinSequence of NAT by Th1;

A2: for k being Nat st k in dom f holds

n divides f . k by Th39;

Sum h = (Sum f) + 2 by Th35;

then 2 |^ n = (Sum f) + 2 by NEWTON:32;

hence n divides (2 |^ n) - 2 by A2, INT_4:36; :: thesis: verum