let a, b, i, m, n be Nat; :: thesis: ( 1 <= i & i <= (len ((a,b) In_Power n)) - m implies a |^ m divides ((a,b) In_Power n) . i )
set P = (a,b) In_Power n;
assume that
A1: 1 <= i and
A2: i <= (len ((a,b) In_Power n)) - m ; :: thesis: a |^ m divides ((a,b) In_Power n) . i
reconsider M = i - 1 as Element of NAT by A1, INT_1:5;
(len ((a,b) In_Power n)) - m <= len ((a,b) In_Power n) by XREAL_1:43;
then A3: i <= len ((a,b) In_Power n) by A2, XXREAL_0:2;
then A4: i in dom ((a,b) In_Power n) by A1, FINSEQ_3:25;
A5: len ((a,b) In_Power n) = n + 1 by NEWTON:def 4;
then i - 1 <= (n + 1) - 1 by A3, XREAL_1:9;
then reconsider L = n - M as Element of NAT by INT_1:5;
((a,b) In_Power n) . i = ((n choose M) * (a |^ L)) * (b |^ M) by A4, NEWTON:def 4
.= (a |^ L) * ((n choose M) * (b |^ M)) ;
then A6: a |^ L divides ((a,b) In_Power n) . i ;
m <= (n + 1) - i by A2, A5, XREAL_1:11;
then a |^ m divides a |^ L by NEWTON:89;
hence a |^ m divides ((a,b) In_Power n) . i by A6, INT_2:9; :: thesis: verum