bcnp1n

Description: Binomial coefficient: N + 1 choose N . (Contributed by NM, 20-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

		Ref	Expression
	Assertion	bcnp1n	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N}) = N + 1$

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
3		bccmpl	$⊢ (N + 1 \in ℕ_{0} \land N \in ℤ) \to (\binom{N + 1}{N}) = (\binom{N + 1}{N + 1 - N})$
4	1 2 3	syl2anc	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N}) = (\binom{N + 1}{N + 1 - N})$
5		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7		pncan2	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - N = 1$
8	5 6 7	sylancl	$⊢ N \in ℕ_{0} \to N + 1 - N = 1$
9	8	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N + 1 - N}) = (\binom{N + 1}{1})$
10		bcn1	$⊢ N + 1 \in ℕ_{0} \to (\binom{N + 1}{1}) = N + 1$
11	1 10	syl	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{1}) = N + 1$
12	4 9 11	3eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N}) = N + 1$

Metamath Proof Explorer