Metamath Proof Explorer

Theorem bcnm1

Description: The binomial coefficent of ( N - 1 ) is N . (Contributed by Scott Fenton, 16-May-2014)

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

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		bccmpl	$⊢ (N \in ℕ_{0} \land 1 \in ℤ) \to (\binom{N}{1}) = (\binom{N}{N - 1})$
3	1 2	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N}{1}) = (\binom{N}{N - 1})$
4		bcn1	$⊢ N \in ℕ_{0} \to (\binom{N}{1}) = N$
5	3 4	eqtr3d	$⊢ N \in ℕ_{0} \to (\binom{N}{N - 1}) = N$