let k be Nat; 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; 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; (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 )
( 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) )
;
(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 FINSEQ_3:25, A1;
then A3a:
k < n
by A2, Th20, XXREAL_0:2;
then A4:
(
k + 1
< n + 1 &
k + 1
> 1 )
by A1, FINSEQ_3:25, NAT_1:13, XREAL_1:6;
A4a:
n - k > k - k
by A3a, XREAL_1:9;
consider l being
Nat such that A4b:
n = k + l
by A3a, NAT_1:10;
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 A4, FINSEQ_3:25;
A7:
((((a,b) In_Power n) | n) /^ 1) . k =
((a,b) In_Power n) . (k + 1)
by A1, Lm5
.=
((n choose k) * (a |^ l)) * (b |^ k)
by A0, A4d, A6, NEWTON:def 4
;
A8:
n divides n choose k
by A3, A3a, Th21;
(
a divides a |^ l &
b divides b |^ k )
by A4a, A4b, A3, NAT_3:3;
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 A8, NAT_3:1;
hence
(n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
by A7;
verum
end;
hence
(n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k
by L1; verum