let k be non zero Nat; :: thesis: for i being Nat
for p being Prime holds (((i * p) + (p -' k)) choose (p -' k)) mod p = 1
let i be Nat; :: thesis: for p being Prime holds (((i * p) + (p -' k)) choose (p -' k)) mod p = 1
let p be Prime; :: thesis: (((i * p) + (p -' k)) choose (p -' k)) mod p = 1

per cases ( p <= k or p > k ) ;

suppose p <= k ; :: thesis: (((i * p) + (p -' k)) choose (p -' k)) mod p = 1

then p -' k = 0 by NAT_2:8;
then (((i * p) + (p -' k)) choose (p -' k)) mod p = 1 mod ((p - 1) + 1) by NEWTON:19;
hence (((i * p) + (p -' k)) choose (p -' k)) mod p = 1 ; :: thesis: verum

end;

suppose B1: p > k ; :: thesis: (((i * p) + (p -' k)) choose (p -' k)) mod p = 1

then p - k > k - k by XREAL_1:9;
then reconsider m = p - k as non zero Nat ;
B2: m + 0 < m + k by XREAL_1:6;
p - k = p -' k by B1, XREAL_1:233;
then (((i * p) + (p -' k)) choose (p -' k)) mod p = ((((i * p) + m) mod p) choose m) mod p by B2, MOC
.= ((m mod p) choose m) mod p by NAT_D:61
.= 1 mod ((p - 1) + 1) by B2, NEWTON:21 ;
hence (((i * p) + (p -' k)) choose (p -' k)) mod p = 1 ; :: thesis: verum

end;

end;