5bc2eq10

		Ref	Expression
	Assertion	5bc2eq10	$⊢ (\binom{5}{2}) = 10$

Step	Hyp	Ref	Expression
1		4nn0	$⊢ 4 \in ℕ_{0}$
2		2z	$⊢ 2 \in ℤ$
3		bcpasc	$⊢ (4 \in ℕ_{0} \land 2 \in ℤ) \to (\binom{4}{2}) + (\binom{4}{2 - 1}) = (\binom{4 + 1}{2})$
4	1 2 3	mp2an	$⊢ (\binom{4}{2}) + (\binom{4}{2 - 1}) = (\binom{4 + 1}{2})$
5		4p1e5	$⊢ 4 + 1 = 5$
6	5	oveq1i	$⊢ (\binom{4 + 1}{2}) = (\binom{5}{2})$
7	4 6	eqtri	$⊢ (\binom{4}{2}) + (\binom{4}{2 - 1}) = (\binom{5}{2})$
8	7	eqcomi	$⊢ (\binom{5}{2}) = (\binom{4}{2}) + (\binom{4}{2 - 1})$
9		2m1e1	$⊢ 2 - 1 = 1$
10	9	oveq2i	$⊢ (\binom{4}{2 - 1}) = (\binom{4}{1})$
11	10	oveq2i	$⊢ (\binom{4}{2}) + (\binom{4}{2 - 1}) = (\binom{4}{2}) + (\binom{4}{1})$
12		4bc2eq6	$⊢ (\binom{4}{2}) = 6$
13		bcn1	$⊢ 4 \in ℕ_{0} \to (\binom{4}{1}) = 4$
14	1 13	ax-mp	$⊢ (\binom{4}{1}) = 4$
15	12 14	oveq12i	$⊢ (\binom{4}{2}) + (\binom{4}{1}) = 6 + 4$
16	11 15	eqtri	$⊢ (\binom{4}{2}) + (\binom{4}{2 - 1}) = 6 + 4$
17		6p4e10	$⊢ 6 + 4 = 10$
18	8 16 17	3eqtri	$⊢ (\binom{5}{2}) = 10$

Metamath Proof Explorer