Metamath Proof Explorer


Theorem bccolsum

Description: A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020)

Ref Expression
Assertion bccolsum ( ( 𝑁 ∈ ℕ0𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑚 = 0 → ( 0 ... 𝑚 ) = ( 0 ... 0 ) )
2 1 sumeq1d ( 𝑚 = 0 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) )
3 oveq1 ( 𝑚 = 0 → ( 𝑚 + 1 ) = ( 0 + 1 ) )
4 0p1e1 ( 0 + 1 ) = 1
5 3 4 eqtrdi ( 𝑚 = 0 → ( 𝑚 + 1 ) = 1 )
6 5 oveq1d ( 𝑚 = 0 → ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) = ( 1 C ( 𝐶 + 1 ) ) )
7 2 6 eqeq12d ( 𝑚 = 0 → ( Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ↔ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) ) )
8 7 imbi2d ( 𝑚 = 0 → ( ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) ) ) )
9 oveq2 ( 𝑚 = 𝑛 → ( 0 ... 𝑚 ) = ( 0 ... 𝑛 ) )
10 9 sumeq1d ( 𝑚 = 𝑛 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) )
11 oveq1 ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
12 11 oveq1d ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) )
13 10 12 eqeq12d ( 𝑚 = 𝑛 → ( Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ↔ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) )
14 13 imbi2d ( 𝑚 = 𝑛 → ( ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) ) )
15 oveq2 ( 𝑚 = ( 𝑛 + 1 ) → ( 0 ... 𝑚 ) = ( 0 ... ( 𝑛 + 1 ) ) )
16 15 sumeq1d ( 𝑚 = ( 𝑛 + 1 ) → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) )
17 oveq1 ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 + 1 ) = ( ( 𝑛 + 1 ) + 1 ) )
18 17 oveq1d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) )
19 16 18 eqeq12d ( 𝑚 = ( 𝑛 + 1 ) → ( Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ↔ Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) ) )
20 19 imbi2d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) ) ) )
21 oveq2 ( 𝑚 = 𝑁 → ( 0 ... 𝑚 ) = ( 0 ... 𝑁 ) )
22 21 sumeq1d ( 𝑚 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) )
23 oveq1 ( 𝑚 = 𝑁 → ( 𝑚 + 1 ) = ( 𝑁 + 1 ) )
24 23 oveq1d ( 𝑚 = 𝑁 → ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) )
25 22 24 eqeq12d ( 𝑚 = 𝑁 → ( Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ↔ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) ) )
26 25 imbi2d ( 𝑚 = 𝑁 → ( ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑚 ) ( 𝑘 C 𝐶 ) = ( ( 𝑚 + 1 ) C ( 𝐶 + 1 ) ) ) ↔ ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) ) ) )
27 0z 0 ∈ ℤ
28 0nn0 0 ∈ ℕ0
29 nn0z ( 𝐶 ∈ ℕ0𝐶 ∈ ℤ )
30 bccl ( ( 0 ∈ ℕ0𝐶 ∈ ℤ ) → ( 0 C 𝐶 ) ∈ ℕ0 )
31 28 29 30 sylancr ( 𝐶 ∈ ℕ0 → ( 0 C 𝐶 ) ∈ ℕ0 )
32 31 nn0cnd ( 𝐶 ∈ ℕ0 → ( 0 C 𝐶 ) ∈ ℂ )
33 oveq1 ( 𝑘 = 0 → ( 𝑘 C 𝐶 ) = ( 0 C 𝐶 ) )
34 33 fsum1 ( ( 0 ∈ ℤ ∧ ( 0 C 𝐶 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) = ( 0 C 𝐶 ) )
35 27 32 34 sylancr ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) = ( 0 C 𝐶 ) )
36 elnn0 ( 𝐶 ∈ ℕ0 ↔ ( 𝐶 ∈ ℕ ∨ 𝐶 = 0 ) )
37 1red ( 𝐶 ∈ ℕ → 1 ∈ ℝ )
38 nnrp ( 𝐶 ∈ ℕ → 𝐶 ∈ ℝ+ )
39 37 38 ltaddrp2d ( 𝐶 ∈ ℕ → 1 < ( 𝐶 + 1 ) )
40 peano2nn ( 𝐶 ∈ ℕ → ( 𝐶 + 1 ) ∈ ℕ )
41 40 nnred ( 𝐶 ∈ ℕ → ( 𝐶 + 1 ) ∈ ℝ )
42 37 41 ltnled ( 𝐶 ∈ ℕ → ( 1 < ( 𝐶 + 1 ) ↔ ¬ ( 𝐶 + 1 ) ≤ 1 ) )
43 39 42 mpbid ( 𝐶 ∈ ℕ → ¬ ( 𝐶 + 1 ) ≤ 1 )
44 elfzle2 ( ( 𝐶 + 1 ) ∈ ( 0 ... 1 ) → ( 𝐶 + 1 ) ≤ 1 )
45 43 44 nsyl ( 𝐶 ∈ ℕ → ¬ ( 𝐶 + 1 ) ∈ ( 0 ... 1 ) )
46 45 iffalsed ( 𝐶 ∈ ℕ → if ( ( 𝐶 + 1 ) ∈ ( 0 ... 1 ) , ( ( ! ‘ 1 ) / ( ( ! ‘ ( 1 − ( 𝐶 + 1 ) ) ) · ( ! ‘ ( 𝐶 + 1 ) ) ) ) , 0 ) = 0 )
47 1nn0 1 ∈ ℕ0
48 40 nnzd ( 𝐶 ∈ ℕ → ( 𝐶 + 1 ) ∈ ℤ )
49 bcval ( ( 1 ∈ ℕ0 ∧ ( 𝐶 + 1 ) ∈ ℤ ) → ( 1 C ( 𝐶 + 1 ) ) = if ( ( 𝐶 + 1 ) ∈ ( 0 ... 1 ) , ( ( ! ‘ 1 ) / ( ( ! ‘ ( 1 − ( 𝐶 + 1 ) ) ) · ( ! ‘ ( 𝐶 + 1 ) ) ) ) , 0 ) )
50 47 48 49 sylancr ( 𝐶 ∈ ℕ → ( 1 C ( 𝐶 + 1 ) ) = if ( ( 𝐶 + 1 ) ∈ ( 0 ... 1 ) , ( ( ! ‘ 1 ) / ( ( ! ‘ ( 1 − ( 𝐶 + 1 ) ) ) · ( ! ‘ ( 𝐶 + 1 ) ) ) ) , 0 ) )
51 bc0k ( 𝐶 ∈ ℕ → ( 0 C 𝐶 ) = 0 )
52 46 50 51 3eqtr4rd ( 𝐶 ∈ ℕ → ( 0 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) )
53 bcnn ( 0 ∈ ℕ0 → ( 0 C 0 ) = 1 )
54 28 53 ax-mp ( 0 C 0 ) = 1
55 bcnn ( 1 ∈ ℕ0 → ( 1 C 1 ) = 1 )
56 47 55 ax-mp ( 1 C 1 ) = 1
57 54 56 eqtr4i ( 0 C 0 ) = ( 1 C 1 )
58 oveq2 ( 𝐶 = 0 → ( 0 C 𝐶 ) = ( 0 C 0 ) )
59 oveq1 ( 𝐶 = 0 → ( 𝐶 + 1 ) = ( 0 + 1 ) )
60 59 4 eqtrdi ( 𝐶 = 0 → ( 𝐶 + 1 ) = 1 )
61 60 oveq2d ( 𝐶 = 0 → ( 1 C ( 𝐶 + 1 ) ) = ( 1 C 1 ) )
62 57 58 61 3eqtr4a ( 𝐶 = 0 → ( 0 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) )
63 52 62 jaoi ( ( 𝐶 ∈ ℕ ∨ 𝐶 = 0 ) → ( 0 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) )
64 36 63 sylbi ( 𝐶 ∈ ℕ0 → ( 0 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) )
65 35 64 eqtrd ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑘 C 𝐶 ) = ( 1 C ( 𝐶 + 1 ) ) )
66 elnn0uz ( 𝑛 ∈ ℕ0𝑛 ∈ ( ℤ ‘ 0 ) )
67 66 biimpi ( 𝑛 ∈ ℕ0𝑛 ∈ ( ℤ ‘ 0 ) )
68 67 adantr ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → 𝑛 ∈ ( ℤ ‘ 0 ) )
69 elfznn0 ( 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) → 𝑘 ∈ ℕ0 )
70 69 adantl ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
71 simplr ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ) → 𝐶 ∈ ℕ0 )
72 71 nn0zd ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ) → 𝐶 ∈ ℤ )
73 bccl ( ( 𝑘 ∈ ℕ0𝐶 ∈ ℤ ) → ( 𝑘 C 𝐶 ) ∈ ℕ0 )
74 70 72 73 syl2anc ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ) → ( 𝑘 C 𝐶 ) ∈ ℕ0 )
75 74 nn0cnd ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ) → ( 𝑘 C 𝐶 ) ∈ ℂ )
76 oveq1 ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C 𝐶 ) )
77 68 75 76 fsump1 ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) + ( ( 𝑛 + 1 ) C 𝐶 ) ) )
78 77 adantr ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) + ( ( 𝑛 + 1 ) C 𝐶 ) ) )
79 id ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) )
80 nn0cn ( 𝐶 ∈ ℕ0𝐶 ∈ ℂ )
81 80 adantl ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
82 1cnd ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
83 81 82 pncand ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → ( ( 𝐶 + 1 ) − 1 ) = 𝐶 )
84 83 oveq2d ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) = ( ( 𝑛 + 1 ) C 𝐶 ) )
85 84 eqcomd ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) C 𝐶 ) = ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) )
86 79 85 oveqan12rd ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) → ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) + ( ( 𝑛 + 1 ) C 𝐶 ) ) = ( ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) + ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) ) )
87 peano2nn0 ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
88 peano2nn0 ( 𝐶 ∈ ℕ0 → ( 𝐶 + 1 ) ∈ ℕ0 )
89 88 nn0zd ( 𝐶 ∈ ℕ0 → ( 𝐶 + 1 ) ∈ ℤ )
90 bcpasc ( ( ( 𝑛 + 1 ) ∈ ℕ0 ∧ ( 𝐶 + 1 ) ∈ ℤ ) → ( ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) + ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) )
91 87 89 90 syl2an ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) → ( ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) + ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) )
92 91 adantr ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) → ( ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) + ( ( 𝑛 + 1 ) C ( ( 𝐶 + 1 ) − 1 ) ) ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) )
93 78 86 92 3eqtrd ( ( ( 𝑛 ∈ ℕ0𝐶 ∈ ℕ0 ) ∧ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) )
94 93 exp31 ( 𝑛 ∈ ℕ0 → ( 𝐶 ∈ ℕ0 → ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) ) ) )
95 94 a2d ( 𝑛 ∈ ℕ0 → ( ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑘 C 𝐶 ) = ( ( 𝑛 + 1 ) C ( 𝐶 + 1 ) ) ) → ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( 𝑘 C 𝐶 ) = ( ( ( 𝑛 + 1 ) + 1 ) C ( 𝐶 + 1 ) ) ) ) )
96 8 14 20 26 65 95 nn0ind ( 𝑁 ∈ ℕ0 → ( 𝐶 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) ) )
97 96 imp ( ( 𝑁 ∈ ℕ0𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑘 C 𝐶 ) = ( ( 𝑁 + 1 ) C ( 𝐶 + 1 ) ) )