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 ) ) )