Metamath Proof Explorer

Theorem bccolsum

Description: A column-sum rule for binomial coefficients. (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 ) ) )