let n be Nat; :: thesis: for a, b being Integer
for k being Nat st k in dom (Newton_Coeff n) holds
(Newton_Coeff n) . k divides ((a,b) In_Power n) . k
let a, b be Integer; :: thesis: for k being Nat st k in dom (Newton_Coeff n) holds
(Newton_Coeff n) . k divides ((a,b) In_Power n) . k
let k be Nat; :: thesis: ( k in dom (Newton_Coeff n) implies (Newton_Coeff n) . k divides ((a,b) In_Power n) . k )
assume A0: k in dom (Newton_Coeff n) ; :: thesis: (Newton_Coeff n) . k divides ((a,b) In_Power n) . k
A0a: k >= 1 by A0, FINSEQ_3:25;
then reconsider m = k - 1 as Nat ;
A1: n + 1 = len ((a,b) In_Power n) by NEWTON:def 4;
len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
then A1a: n + 1 >= m + 1 by A0, FINSEQ_3:25;
then consider l being Nat such that
A2: n = m + l by XREAL_1:6, NAT_1:10;
A3: (Newton_Coeff n) . k = n choose m by A0, NEWTON:def 5;
A4: k in dom ((a,b) In_Power n) by A0a, A1, A1a, FINSEQ_3:25;
l = n - m by A2;
then ((a,b) In_Power n) . k = ((n choose m) * (a |^ l)) * (b |^ m) by A4, NEWTON:def 4
.= ((Newton_Coeff n) . k) * ((a |^ l) * (b |^ m)) by A3 ;
hence (Newton_Coeff n) . k divides ((a,b) In_Power n) . k ; :: thesis: verum