let n, k be Nat; :: thesis: ( n is prime & k <> 0 & k <> n implies n divides n choose k )

assume A1: ( n is prime & k <> 0 & k <> n ) ; :: thesis: n divides n choose k

assume A1: ( n is prime & k <> 0 & k <> n ) ; :: thesis: n divides n choose k

per cases then
( k > n or k < n )
by XXREAL_0:1;

end;

suppose B1:
k < n
; :: thesis: n divides n choose k

then consider m being Nat such that

B1a: n = 1 + m by NAT_1:14, NAT_1:10;

B1b: k ! ,n are_coprime by A1, B1, NAT_4:19, GROUP_17:5;

consider l being Nat such that

B2: n = k + l by B1, NAT_1:10;

k + l > 0 + l by A1, XREAL_1:6;

then B3a: l ! ,n are_coprime by A1, B2, NAT_4:19, GROUP_17:5;

l = n - k by B2;

then n choose k = (n !) / ((k !) * (l !)) by B1, NEWTON:def 3;

then (n choose k) * ((k !) * (l !)) = n ! by XCMPLX_1:87;

then (n choose k) * ((k !) * (l !)) = (m !) * n by B1a, NEWTON:15;

then n divides ((n choose k) * (k !)) * (l !) ;

then n divides (n choose k) * (k !) by B3a, INT_2:25;

hence n divides n choose k by B1b, INT_2:25; :: thesis: verum

end;B1a: n = 1 + m by NAT_1:14, NAT_1:10;

B1b: k ! ,n are_coprime by A1, B1, NAT_4:19, GROUP_17:5;

consider l being Nat such that

B2: n = k + l by B1, NAT_1:10;

k + l > 0 + l by A1, XREAL_1:6;

then B3a: l ! ,n are_coprime by A1, B2, NAT_4:19, GROUP_17:5;

l = n - k by B2;

then n choose k = (n !) / ((k !) * (l !)) by B1, NEWTON:def 3;

then (n choose k) * ((k !) * (l !)) = n ! by XCMPLX_1:87;

then (n choose k) * ((k !) * (l !)) = (m !) * n by B1a, NEWTON:15;

then n divides ((n choose k) * (k !)) * (l !) ;

then n divides (n choose k) * (k !) by B3a, INT_2:25;

hence n divides n choose k by B1b, INT_2:25; :: thesis: verum