let n, k be Nat; ( 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 )
( 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 )
;
n divides (((Newton_Coeff n) | n) /^ 1) . k
per cases
( k > 0 or k = 0 )
;
suppose A1aa:
k > 0
;
n divides (((Newton_Coeff n) | n) /^ 1) . kthen 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;
verum end; end;
end;
hence
( n is prime implies n divides (((Newton_Coeff n) | n) /^ 1) . k )
by L1; verum