let k be Nat; :: thesis: for n being prime Nat
for a, b being positive Nat holds (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k

let n be prime Nat; :: thesis: for a, b being positive Nat holds (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
let a, b be positive Nat; :: thesis: (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
L1: ( not k in dom ((((a,b) In_Power n) | n) /^ 1) implies (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k )
proof
assume not k in dom ((((a,b) In_Power n) | n) /^ 1) ; :: thesis: (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
then ((((a,b) In_Power n) | n) /^ 1) . k = {} by FUNCT_1:def 2;
hence (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k by NAT_D:6; :: thesis: verum
end;
( n is prime & k in dom ((((a,b) In_Power n) | n) /^ 1) implies (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k )
proof
A0: k = (k + 1) - 1 ;
assume A1: ( n is prime & k in dom ((((a,b) In_Power n) | n) /^ 1) ) ; :: thesis: (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
then A2: not (((a,b) In_Power n) | n) /^ 1 is empty ;
A3: ( k >= 1 & k <= len ((((a,b) In_Power n) | n) /^ 1) ) by ;
then A3a: k < n by ;
then A4: ( k + 1 < n + 1 & k + 1 > 1 ) by ;
A4a: n - k > k - k by ;
consider l being Nat such that
A4b: n = k + l by ;
A4d: l = n - k by A4b;
len ((a,b) In_Power n) = n + 1 by NEWTON:def 4;
then A6: k + 1 in dom ((a,b) In_Power n) by ;
A7: ((((a,b) In_Power n) | n) /^ 1) . k = ((a,b) In_Power n) . (k + 1) by
.= ((n choose k) * (a |^ l)) * (b |^ k) by ;
A8: n divides n choose k by ;
( a divides a |^ l & b divides b |^ k ) by ;
then a * b divides (a |^ l) * (b |^ k) by NAT_3:1;
then n * (a * b) divides (n choose k) * ((a |^ l) * (b |^ k)) by ;
hence (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k by A7; :: thesis: verum
end;
hence (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k by L1; :: thesis: verum