let n, k be Nat; :: thesis: for p being Prime st k < p holds
(((n * p) + k) choose k) mod p = 1
let p be Prime; :: thesis: ( k < p implies (((n * p) + k) choose k) mod p = 1 )
assume A1: k < p ; :: thesis: (((n * p) + k) choose k) mod p = 1
(((n * p) + k) choose k) mod p = ((((n * p) + k) mod p) choose k) mod p by A1, MOC
.= ((k mod p) choose k) mod p by NAT_D:61
.= (k choose k) mod p by A1, MOC
.= 1 mod (1 + (p - 1)) by NEWTON:21 ;
hence (((n * p) + k) choose k) mod p = 1 ; :: thesis: verum