let n, k, u be Nat; :: thesis: ( u > n |^ k & n >= k implies [\(((u + 1) |^ n) / (u |^ k))/] mod u = n choose k )

assume A1: ( u > n |^ k & n >= k ) ; :: thesis: [\(((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

(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 S_{1}[ 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 S_{1}[j,x]

A29: dom Q = Seg (len q) and

A30: for j being Nat st j in Seg (len q) holds

S_{1}[j,Q . j]
from FINSEQ_1:sch 1(A21);

rng Q c= NAT

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 A33: Sum q = ((u |^ k) * u) * (Sum Q) by RVSUM_1:87;

A34: [\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q))

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; :: thesis: verum

assume A1: ( u > n |^ k & n >= k ) ; :: thesis: [\(((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

then A17:
for i being Nat st i in Seg k holds
let i be Nat; :: thesis: ( i in Seg k implies (I1 | k) . i < (k |-> ((u |^ k) / n)) . i )

assume A9: i in Seg k ; :: thesis: (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; :: thesis: verum

end;assume A9: i in Seg k ; :: thesis: (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; :: thesis: verum

(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 S

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 S

proof

consider Q being FinSequence such that
let j be Nat; :: thesis: ( j in Seg (len q) implies ex x being object st S_{1}[j,x] )

assume A22: j in Seg (len q) ; :: thesis: ex x being object st S_{1}[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); :: thesis: S_{1}[j,U]

thus S_{1}[j,U]
by A27, A28, A23, FINSEQ_1:65, A2, A4, ORDINAL1:def 12; :: thesis: verum

end;assume A22: j in Seg (len q) ; :: thesis: ex x being object st S

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); :: thesis: S

thus S

A29: dom Q = Seg (len q) and

A30: for j being Nat st j in Seg (len q) holds

S

rng Q c= NAT

proof

then reconsider Q = Q as FinSequence of NAT by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng Q or y in NAT )

assume A31: y in rng Q ; :: thesis: y in NAT

ex x being object st

( x in dom Q & Q . x = y ) by FUNCT_1:def 3, A31;

hence y in NAT by A30, A29; :: thesis: verum

end;assume A31: y in rng Q ; :: thesis: y in NAT

ex x being object st

( x in dom Q & Q . x = y ) by FUNCT_1:def 3, A31;

hence y in NAT by A30, A29; :: thesis: verum

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

proof

then
q = ((u |^ k) * u) * Q
by A32, FINSEQ_1:14;
let i be Nat; :: thesis: ( 1 <= i & i <= len q implies q . i = (((u |^ k) * u) * Q) . i )

assume ( 1 <= i & i <= len q ) ; :: thesis: q . i = (((u |^ k) * u) * Q) . i

then i in dom Q by A29;

then q . i = ((u |^ k) * u) * (Q . i) by A29, A30;

hence q . i = (((u |^ k) * u) * Q) . i by VALUED_1:6; :: thesis: verum

end;assume ( 1 <= i & i <= len q ) ; :: thesis: q . i = (((u |^ k) * u) * Q) . i

then i in dom Q by A29;

then q . i = ((u |^ k) * u) * (Q . i) by A29, A30;

hence q . i = (((u |^ k) * u) * Q) . i by VALUED_1:6; :: thesis: verum

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
end;

A43:
Sum I1 = (1 + u) |^ n
by NEWTON:30;per cases
( k = 0 or k >= 1 )
by NAT_1:14;

end;

suppose
k = 0
; :: thesis: [\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q))

then
Sum (I1 | k) = 0
by RVSUM_1:72;

then 1 * (Sum I1) = (u |^ k) * ((n choose k) + (u * (Sum Q))) by A33, A19, A6;

then (Sum I1) / (u |^ k) = ((n choose k) + (u * (Sum Q))) / 1 by A1, XCMPLX_1:94;

hence [\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q)) by INT_1:25; :: thesis: verum

end;then 1 * (Sum I1) = (u |^ k) * ((n choose k) + (u * (Sum Q))) by A33, A19, A6;

then (Sum I1) / (u |^ k) = ((n choose k) + (u * (Sum Q))) / 1 by A1, XCMPLX_1:94;

hence [\((Sum I1) / (u |^ k))/] = (n choose k) + (u * (Sum Q)) by INT_1:25; :: thesis: verum

suppose A35:
k >= 1
; :: thesis: [\((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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum