bcnn

Description: N choose N is 1. Remark in Gleason p. 296. (Contributed by NM, 17-Jun-2005) (Revised by Mario Carneiro, 8-Nov-2013)

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

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		bccmpl	$⊢ (N \in ℕ_{0} \land 0 \in ℤ) \to (\binom{N}{0}) = (\binom{N}{N - 0})$
3	1 2	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) = (\binom{N}{N - 0})$
4		bcn0	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) = 1$
5		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
6	5	subid1d	$⊢ N \in ℕ_{0} \to N - 0 = N$
7	6	oveq2d	$⊢ N \in ℕ_{0} \to (\binom{N}{N - 0}) = (\binom{N}{N})$
8	3 4 7	3eqtr3rd	$⊢ N \in ℕ_{0} \to (\binom{N}{N}) = 1$

Metamath Proof Explorer