Theorem 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 {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{N}{0}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		0elfz	$$⊢N\in {\mathbb{N}}_0\to 0\in \left(0\dots N\right)$$
2		bcval2	$$⊢0\in \left(0\dots N\right)\to \left(\genfrac{}{}{0ex}{}{N}{0}\right)=\frac{N!}{\left(N-0\right)!0!}$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{N}{0}\right)=\frac{N!}{\left(N-0\right)!0!}$$
4		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
5	4	subid1d	$$⊢N\in {\mathbb{N}}_0\to N-0=N$$
6	5	fveq2d	$$⊢N\in {\mathbb{N}}_0\to \left(N-0\right)!=N!$$
7		fac0	$$⊢0!=1$$
8		oveq12	$$⊢\left(\left(N-0\right)!=N!\wedge 0!=1\right)\to \left(N-0\right)!0!=N!\cdot 1$$
9	6 7 8	sylancl	$$⊢N\in {\mathbb{N}}_0\to \left(N-0\right)!0!=N!\cdot 1$$
10		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
11	10	nncnd	$$⊢N\in {\mathbb{N}}_0\to N!\in ℂ$$
12	11	mulid1d	$$⊢N\in {\mathbb{N}}_0\to N!\cdot 1=N!$$
13	9 12	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(N-0\right)!0!=N!$$
14	13	oveq2d	$$⊢N\in {\mathbb{N}}_0\to \frac{N!}{\left(N-0\right)!0!}=\frac{N!}{N!}$$
15		facne0	$$⊢N\in {\mathbb{N}}_0\to N!\ne 0$$
16	11 15	dividd	$$⊢N\in {\mathbb{N}}_0\to \frac{N!}{N!}=1$$
17	14 16	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \frac{N!}{\left(N-0\right)!0!}=1$$
18	3 17	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \left(\genfrac{}{}{0ex}{}{N}{0}\right)=1$$