ex-bc

		Ref	Expression
	Assertion	ex-bc	$⊢ (\binom{5}{3}) = 10$

Step	Hyp	Ref	Expression
1		df-5	$⊢ 5 = 4 + 1$
2	1	oveq1i	$⊢ (\binom{5}{3}) = (\binom{4 + 1}{3})$
3		4bc3eq4	$⊢ (\binom{4}{3}) = 4$
4		3m1e2	$⊢ 3 - 1 = 2$
5	4	oveq2i	$⊢ (\binom{4}{3 - 1}) = (\binom{4}{2})$
6		4bc2eq6	$⊢ (\binom{4}{2}) = 6$
7	5 6	eqtri	$⊢ (\binom{4}{3 - 1}) = 6$
8	3 7	oveq12i	$⊢ (\binom{4}{3}) + (\binom{4}{3 - 1}) = 4 + 6$
9		4nn0	$⊢ 4 \in ℕ_{0}$
10		3z	$⊢ 3 \in ℤ$
11		bcpasc	$⊢ (4 \in ℕ_{0} \land 3 \in ℤ) \to (\binom{4}{3}) + (\binom{4}{3 - 1}) = (\binom{4 + 1}{3})$
12	9 10 11	mp2an	$⊢ (\binom{4}{3}) + (\binom{4}{3 - 1}) = (\binom{4 + 1}{3})$
13		6cn	$⊢ 6 \in ℂ$
14		4cn	$⊢ 4 \in ℂ$
15		6p4e10	$⊢ 6 + 4 = 10$
16	13 14 15	addcomli	$⊢ 4 + 6 = 10$
17	8 12 16	3eqtr3i	$⊢ (\binom{4 + 1}{3}) = 10$
18	2 17	eqtri	$⊢ (\binom{5}{3}) = 10$

Metamath Proof Explorer