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

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