let n, k, u be Nat; ( u > n |^ k & n >= k implies [\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k )
assume A1:
( u > n |^ k & n >= k )
; [\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k
set I = (1,u) In_Power n;
set k1 = k + 1;
consider q being FinSequence such that
A2:
(1,u) In_Power n = (((1,u) In_Power n) | (k + 1)) ^ q
by FINSEQ_1:80;
rng ((1,u) In_Power n) c= NAT
by VALUED_0:def 6;
then reconsider I1 = (1,u) In_Power n as FinSequence of NAT by FINSEQ_1:def 4;
I1 = (I1 | (k + 1)) ^ q
by A2;
then reconsider q = q as FinSequence of NAT by FINSEQ_1:36;
A3:
len I1 = n + 1
by NEWTON:def 4;
A4:
len (I1 | (k + 1)) = k + 1
by A1, XREAL_1:7, A3, FINSEQ_1:59;
1 <= k + 1
by NAT_1:11;
then
k + 1 in dom ((1,u) In_Power n)
by A3, A1, XREAL_1:7, FINSEQ_3:25;
then A5:
I1 | (k + 1) = (I1 | k) ^ <*(I1 . (k + 1))*>
by FINSEQ_5:10;
A6: Sum I1 =
(Sum (I1 | (k + 1))) + (Sum q)
by A2, RVSUM_1:75
.=
((Sum (I1 | k)) + (I1 . (k + 1))) + (Sum q)
by A5, RVSUM_1:74
;
k <= n + 1
by A1, NAT_1:13;
then A7:
I1 | k is k -element
by A3, FINSEQ_1:59;
set kI = k |-> ((u |^ k) / n);
A8:
for i being Nat st i in Seg k holds
(I1 | k) . i < (k |-> ((u |^ k) / n)) . i
proof
let i be
Nat;
( i in Seg k implies (I1 | k) . i < (k |-> ((u |^ k) / n)) . i )
assume A9:
i in Seg k
;
(I1 | k) . i < (k |-> ((u |^ k) / n)) . i
A10:
(k |-> ((u |^ k) / n)) . i = (u |^ k) / n
by A9, FINSEQ_2:57;
A11:
( 1
<= i &
i <= k )
by A9, FINSEQ_1:1;
then A12:
(I1 | k) . i = I1 . i
by FINSEQ_3:112;
reconsider i1 =
i - 1 as
Nat by A11;
set ni =
n -' i1;
A13:
(
i1 + 1
= i &
i <= n )
by A11, A1, XXREAL_0:2;
then A14:
(
i1 < n &
i <= n + 1 )
by NAT_1:13;
then A15:
i in dom I1
by A11, A3, FINSEQ_3:25;
n -' i1 = n - i1
by A14, XREAL_1:233;
then A16:
I1 . i = ((n choose i1) * (1 |^ (n -' i1))) * (u |^ i1)
by A15, NEWTON:def 4;
k > i1
by A13, A11, NAT_1:13;
hence
(I1 | k) . i < (k |-> ((u |^ k) / n)) . i
by Th14, A1, A10, A16, A12;
verum
end;
then A17:
for i being Nat st i in Seg k holds
(I1 | k) . i <= (k |-> ((u |^ k) / n)) . i
;
1 <= k + 1
by NAT_1:11;
then A18:
k + 1 in dom I1
by A1, XREAL_1:7, A3, FINSEQ_3:25;
( n - k = n -' k & k = (k + 1) - 1 )
by A1, XREAL_1:233;
then A19:
I1 . (k + 1) = ((n choose k) * (1 |^ (n -' k))) * (u |^ k)
by A18, NEWTON:def 4;
defpred S1[ Nat, object ] means ( $2 in NAT & ( for i being Nat st i = $2 holds
q . $1 = ((u |^ k) * u) * i ) );
len ((1,u) In_Power n) = (k + 1) + (len q)
by A2, A4, FINSEQ_1:22;
then A20:
n = k + (len q)
by A3;
A21:
for j being Nat st j in Seg (len q) holds
ex x being object st S1[j,x]
proof
let j be
Nat;
( j in Seg (len q) implies ex x being object st S1[j,x] )
assume A22:
j in Seg (len q)
;
ex x being object st S1[j,x]
A23:
( 1
<= j &
j <= len q )
by FINSEQ_1:1, A22;
A24:
((k + 1) + j) - 1
= k + j
;
A25:
n >= k + j
by A23, A20, XREAL_1:7;
A26:
n -' (k + j) = n - (k + j)
by XREAL_1:233, A23, A20, XREAL_1:7;
( 1
<= (k + j) + 1 &
(k + j) + 1
<= n + 1 )
by NAT_1:11, A25, XREAL_1:7;
then
(k + 1) + j in dom I1
by FINSEQ_3:25, A3;
then A27:
I1 . ((k + 1) + j) = ((n choose (k + j)) * (1 |^ (n -' (k + j)))) * (u |^ (k + j))
by A24, A26, NEWTON:def 4;
reconsider j1 =
j - 1 as
Nat by A23;
A28:
u |^ (k + j) =
(u |^ k) * (u |^ (j1 + 1))
by NEWTON:8
.=
(u |^ k) * ((u |^ j1) * u)
by NEWTON:6
;
take U =
((n choose (k + j)) * (1 |^ (n -' (k + j)))) * (u |^ j1);
S1[j,U]
thus
S1[
j,
U]
by A27, A28, A23, FINSEQ_1:65, A2, A4, ORDINAL1:def 12;
verum
end;
consider Q being FinSequence such that
A29:
dom Q = Seg (len q)
and
A30:
for j being Nat st j in Seg (len q) holds
S1[j,Q . j]
from FINSEQ_1:sch 1(A21);
rng Q c= NAT
then reconsider Q = Q as FinSequence of NAT by FINSEQ_1:def 4;
A32:
( len Q = len q & len (((u |^ k) * u) * Q) = len Q )
by CARD_1:def 7, A29, FINSEQ_1:def 3;
for i being Nat st 1 <= i & i <= len q holds
q . i = (((u |^ k) * u) * Q) . i
then
q = ((u |^ k) * u) * Q
by A32, FINSEQ_1:14;
then A33:
Sum q = ((u |^ k) * u) * (Sum Q)
by RVSUM_1:87;
A34:
[\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q))
proof
per cases
( k = 0 or k >= 1 )
by NAT_1:14;
suppose A35:
k >= 1
;
[\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q))then A36:
k in Seg k
;
then A37:
(I1 | k) . k < (k |-> ((u |^ k) / n)) . k
by A8;
A38:
Sum (k |-> ((u |^ k) / n)) =
k * ((u |^ k) / n)
by RVSUM_1:80
.=
(u |^ k) * (k / n)
by XCMPLX_1:75
;
Sum (I1 | k) < (u |^ k) * (k / n)
by A37, A36, A7, A17, RVSUM_1:83, A38;
then A39:
(Sum (I1 | k)) + ((I1 . (k + 1)) + (Sum q)) < ((u |^ k) * (k / n)) + ((I1 . (k + 1)) + (Sum q))
by XREAL_1:8;
((u |^ k) * (k / n)) + ((I1 . (k + 1)) + (Sum q)) = (u |^ k) * (((k / n) + (n choose k)) + (u * (Sum Q)))
by A33, A19;
then A40:
(Sum I1) / (u |^ k) < ((k / n) + (n choose k)) + (u * (Sum Q))
by A1, A39, A6, XREAL_1:83;
(
k / n <= n / n &
n / n = 1 )
by A35, XREAL_1:72, A1, XCMPLX_1:60;
then
(k / n) + ((n choose k) + (u * (Sum Q))) <= 1
+ ((n choose k) + (u * (Sum Q)))
by XREAL_1:7;
then
(Sum I1) / (u |^ k) < 1
+ ((n choose k) + (u * (Sum Q)))
by A40, XXREAL_0:2;
then A41:
((Sum I1) / (u |^ k)) - 1
< (n choose k) + (u * (Sum Q))
by XREAL_1:19;
A42:
0 + ((I1 . (k + 1)) + (Sum q)) <= (Sum (I1 | k)) + ((I1 . (k + 1)) + (Sum q))
by XREAL_1:7;
(I1 . (k + 1)) + (Sum q) = (u |^ k) * ((n choose k) + (u * (Sum Q)))
by A33, A19;
then
(Sum I1) / (u |^ k) >= (n choose k) + (u * (Sum Q))
by A1, A42, A6, XREAL_1:77;
hence
[\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q))
by A41, INT_1:def 6;
verum end;
end;
A43:
Sum I1 = (1 + u) |^ n
by NEWTON:30;
n choose k <= n |^ k
by Th13, A1;
then
n choose k < u
by A1, XXREAL_0:2;
then
(n choose k) mod u = n choose k
by NAT_D:24;
hence
[\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k
by A34, A43, NAT_D:21; verum