let b, k, n be Nat; for a being non zero Integer st 1 <= k & k <= n holds
a divides ((a,b) Subnomial n) . k
let a be non zero Integer; ( 1 <= k & k <= n implies a divides ((a,b) Subnomial n) . k )
A0:
len ((a,b) Subnomial n) = n + 1
by Def2;
assume A1:
( 1 <= k & k <= n )
; a divides ((a,b) Subnomial n) . k
then reconsider m = k - 1 as Nat ;
(k - 1) + 1 > (k - 1) + 0
by XREAL_1:6;
then consider l being Nat such that
A2:
n = m + l
by A1, XXREAL_0:2, NAT_1:10;
m + l >= m + 1
by A1, A2;
then
l >= 1
by XREAL_1:6;
then reconsider s = l - 1 as Nat ;
A4:
l = n - m
by A2;
k + 0 <= n + 1
by XREAL_1:7, A1;
then
k in dom ((a,b) Subnomial n)
by A0, A1, FINSEQ_3:25;
then ((a,b) Subnomial n) . k =
(a |^ (s + 1)) * (b |^ m)
by Def2, A4
.=
(a * (a |^ s)) * (b |^ m)
by NEWTON:6
.=
a * ((a |^ s) * (b |^ m))
;
hence
a divides ((a,b) Subnomial n) . k
; verum