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