let p be Prime; :: thesis: for k being non zero Nat st k <> p holds
(p choose k) mod p = 0
let k be non zero Nat; :: thesis: ( k <> p implies (p choose k) mod p = 0 )
assume A1: k <> p ; :: thesis: (p choose k) mod p = 0
p divides p choose k by A1, NEWTON02:119;
hence (p choose k) mod p = 0 by PEPIN:6; :: thesis: verum