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
per cases then ( k > n or k < n ) by XXREAL_0:1;
suppose k > n ; :: thesis: n divides n choose k
then n choose k = 0 by NEWTON:def 3;
hence n divides n choose k by NAT_D:6; :: thesis: verum
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;
end;