let p be Prime; :: thesis: for n being Nat st not p divides n holds
(p choose n) mod p = 0
let n be Nat; :: thesis: ( not p divides n implies (p choose n) mod p = 0 )
assume A1: not p divides n ; :: thesis: (p choose n) mod p = 0
( p divides p * 0 & p divides p * 1 ) ;
then p divides p choose n by A1, NEWTON02:119;
hence (p choose n) mod p = 0 by PEPIN:6; :: thesis: verum