bcp1m1

Description: Compute the binomial coefficient of ( N + 1 ) over ( N - 1 ) (Contributed by Scott Fenton, 11-May-2014) (Revised by Mario Carneiro, 22-May-2014)

		Ref	Expression
	Assertion	bcp1m1	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N - 1}) = \frac{(N + 1) \cdot N}{2}$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
4	2 3	syl	$⊢ N \in ℕ_{0} \to N - 1 \in ℤ$
5		bccmpl	$⊢ (N + 1 \in ℕ_{0} \land N - 1 \in ℤ) \to (\binom{N + 1}{N - 1}) = (\binom{N + 1}{N + 1 - (N - 1)})$
6	1 4 5	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N - 1}) = (\binom{N + 1}{N + 1 - (N - 1)})$
7		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
8		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
9	7 8 8	pnncand	$⊢ N \in ℕ_{0} \to N + 1 - (N - 1) = 1 + 1$
10		df-2	$⊢ 2 = 1 + 1$
11	9 10	eqtr4di	$⊢ N \in ℕ_{0} \to N + 1 - (N - 1) = 2$
12	11	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N + 1 - (N - 1)}) = (\binom{N + 1}{2})$
13		bcn2	$⊢ N + 1 \in ℕ_{0} \to (\binom{N + 1}{2}) = \frac{(N + 1) (N + 1 - 1)}{2}$
14	1 13	syl	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{2}) = \frac{(N + 1) (N + 1 - 1)}{2}$
15		ax-1cn	$⊢ 1 \in ℂ$
16		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
17	7 15 16	sylancl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
18	17	oveq2d	$⊢ N \in ℕ_{0} \to (N + 1) (N + 1 - 1) = (N + 1) \cdot N$
19	18	oveq1d	$⊢ N \in ℕ_{0} \to \frac{(N + 1) (N + 1 - 1)}{2} = \frac{(N + 1) \cdot N}{2}$
20	14 19	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{2}) = \frac{(N + 1) \cdot N}{2}$
21	12 20	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N + 1 - (N - 1)}) = \frac{(N + 1) \cdot N}{2}$
22	6 21	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N - 1}) = \frac{(N + 1) \cdot N}{2}$

Metamath Proof Explorer

Theorem bcp1m1

Proof