bcn0

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

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

Step	Hyp	Ref	Expression
1		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
2		bcval2	$⊢ 0 \in (0 \dots N) \to (\binom{N}{0}) = \frac{N!}{(N - 0)! 0!}$
3	1 2	syl	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) = \frac{N!}{(N - 0)! 0!}$
4		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
5	4	subid1d	$⊢ N \in ℕ_{0} \to N - 0 = N$
6	5	fveq2d	$⊢ N \in ℕ_{0} \to (N - 0)! = N!$
7		fac0	$⊢ 0! = 1$
8		oveq12	$⊢ ((N - 0)! = N! \land 0! = 1) \to (N - 0)! 0! = N! \cdot 1$
9	6 7 8	sylancl	$⊢ N \in ℕ_{0} \to (N - 0)! 0! = N! \cdot 1$
10		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
11	10	nncnd	$⊢ N \in ℕ_{0} \to N! \in ℂ$
12	11	mulridd	$⊢ N \in ℕ_{0} \to N! \cdot 1 = N!$
13	9 12	eqtrd	$⊢ N \in ℕ_{0} \to (N - 0)! 0! = N!$
14	13	oveq2d	$⊢ N \in ℕ_{0} \to \frac{N!}{(N - 0)! 0!} = \frac{N!}{N!}$
15		facne0	$⊢ N \in ℕ_{0} \to N! \neq 0$
16	11 15	dividd	$⊢ N \in ℕ_{0} \to \frac{N!}{N!} = 1$
17	14 16	eqtrd	$⊢ N \in ℕ_{0} \to \frac{N!}{(N - 0)! 0!} = 1$
18	3 17	eqtrd	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) = 1$

Metamath Proof Explorer