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 )

L1: ( n is prime & k >= n implies n divides (((Newton_Coeff n) | n) /^ 1) . k )

proof

( n is prime & k < n implies n divides (((Newton_Coeff n) | n) /^ 1) . k )
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;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

proof

hence
( n is prime implies n divides (((Newton_Coeff n) | n) /^ 1) . k )
by L1; :: thesis: verum
A0:
k = (k + 1) - 1
;

assume A1: ( n is prime & k < n ) ; :: thesis: n divides (((Newton_Coeff n) | n) /^ 1) . k

end;assume A1: ( n is prime & k < n ) ; :: thesis: n divides (((Newton_Coeff n) | n) /^ 1) . k

per cases
( k > 0 or k = 0 )
;

end;

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;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

suppose
k = 0
; :: thesis: n divides (((Newton_Coeff n) | n) /^ 1) . k

then
not k in dom (((Newton_Coeff n) | n) /^ 1)
by FINSEQ_3:25;

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;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