let n, k be Nat; :: thesis: ( n is prime implies n divides ((() | n) /^ 1) . k )
L1: ( n is prime & k >= n implies n divides ((() | n) /^ 1) . k )
proof
assume A1: ( n is prime & k >= n ) ; :: thesis: n divides ((() | n) /^ 1) . k
then n in dom () by Th30;
then k >= len (() | n) by ;
then k + 1 > len (() | n) by NAT_1:13;
then not k + 1 in dom (() | n) by FINSEQ_3:25;
then not k in dom ((() | n) /^ 1) by FINSEQ_5:26;
then (((Newton_Coeff n) | n) /^ 1) . k = {} by FUNCT_1:def 2;
hence n divides ((() | n) /^ 1) . k by NAT_D:6; :: thesis: verum
end;
( n is prime & k < n implies n divides ((() | n) /^ 1) . k )
proof
A0: k = (k + 1) - 1 ;
assume A1: ( n is prime & k < n ) ; :: thesis: n divides ((() | n) /^ 1) . k
per cases ( k > 0 or k = 0 ) ;
suppose A1aa: k > 0 ; :: thesis: n divides ((() | n) /^ 1) . k
then A1a: ( k + 1 > 0 + 1 & k + 1 < n + 1 & len () = n + 1 ) by ;
then A2: k + 1 in dom () by FINSEQ_3:25;
n in dom () by ;
then A3: len (() | n) = n by Th10;
k + 1 <= n by ;
then k + 1 in dom (() | n) by ;
then k in dom ((() | n) /^ 1) by ;
then ((() | n) /^ 1) . k = () . (k + 1) by Th38
.= n choose k by ;
hence n divides ((() | n) /^ 1) . k by ; :: thesis: verum
end;
suppose k = 0 ; :: thesis: n divides ((() | n) /^ 1) . k
then not k in dom ((() | n) /^ 1) by FINSEQ_3:25;
then (((Newton_Coeff n) | n) /^ 1) . k = {} by FUNCT_1:def 2;
hence n divides ((() | n) /^ 1) . k by NAT_D:6; :: thesis: verum
end;
end;
end;
hence ( n is prime implies n divides ((() | n) /^ 1) . k ) by L1; :: thesis: verum