let p be Prime; :: thesis: for k, n being Nat
for m being non zero Nat st k + m < p holds
(((n * p) + k) choose (m + k)) mod p = 0
defpred S₁[ Nat] means for k being Nat
for m being non zero Nat st k + m < p holds
((($1 * p) + k) choose (m + k)) mod p = 0 ;
A1: S₁[ 0 ]

proof

let k be Nat; :: thesis: for m being non zero Nat st k + m < p holds
(((0 * p) + k) choose (m + k)) mod p = 0
let m be non zero Nat; :: thesis: ( k + m < p implies (((0 * p) + k) choose (m + k)) mod p = 0 )
((0 + k) choose (k + m)) mod p = 0 mod p ;
hence ( k + m < p implies (((0 * p) + k) choose (m + k)) mod p = 0 ) ; :: thesis: verum

end;

A2: for q being Nat st S₁[q] holds
S₁[q + 1]

proof

let q be Nat; :: thesis: ( S₁[q] implies S₁[q + 1] )
assume S₁[q] ; :: thesis: S₁[q + 1]
S₁[q + 1]

proof

defpred S₂[ Nat] means for m being non zero Nat st $1 + m < p holds
((((q + 1) * p) + $1) choose (m + $1)) mod p = 0 ;
C1: S₂[ 0 ]

proof

let m be non zero Nat; :: thesis: ( 0 + m < p implies ((((q + 1) * p) + 0) choose (m + 0)) mod p = 0 )
assume D1: 0 + m < p ; :: thesis: ((((q + 1) * p) + 0) choose (m + 0)) mod p = 0
((((q + 1) * p) + 0) choose (m + 0)) mod p = (((((q + 1) * p) + 0) mod p) choose m) mod p by D1, MOC
.= 0 mod p ;
hence ((((q + 1) * p) + 0) choose (m + 0)) mod p = 0 ; :: thesis: verum

end;

C2: for a being Nat st S₂[a] holds
S₂[a + 1]

proof

let a be Nat; :: thesis: ( S₂[a] implies S₂[a + 1] )
S₂[a + 1]

proof

let m be non zero Nat; :: thesis: ( (a + 1) + m < p implies ((((q + 1) * p) + (a + 1)) choose (m + (a + 1))) mod p = 0 )
assume E1: (a + 1) + m < p ; :: thesis: ((((q + 1) * p) + (a + 1)) choose (m + (a + 1))) mod p = 0
(a + 1) + 0 < (a + 1) + m by XREAL_1:6;
then E3: a + 1 < p by E1, XXREAL_0:2;
((((q + 1) * p) + (a + 1)) choose (m + (a + 1))) mod p = (((((q + 1) * p) + (a + 1)) mod p) choose (m + (a + 1))) mod p by E1, MOC
.= (((a + 1) mod p) choose ((a + m) + 1)) mod p by NAT_D:61
.= ((a + 1) choose ((a + 1) + m)) mod p by E3, NAT_D:24
.= 0 mod p ;
hence ((((q + 1) * p) + (a + 1)) choose (m + (a + 1))) mod p = 0 ; :: thesis: verum

end;

hence ( S₂[a] implies S₂[a + 1] ) ; :: thesis: verum

end;

for b being Nat holds S₂[b] from NAT_1:sch 2(C1, C2);
hence S₁[q + 1] ; :: thesis: verum

end;

hence S₁[q + 1] ; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(A1, A2);
hence for k, n being Nat
for m being non zero Nat st k + m < p holds
(((n * p) + k) choose (m + k)) mod p = 0 ; :: thesis: verum