Theorem fac0

Description: The factorial of 0. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	fac0	$$⊢0!=1$$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$$⊢0\in \mathrm{V}$$
2	1	a1i	$$⊢\top \to 0\in \mathrm{V}$$
3		1ex	$$⊢1\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to 1\in \mathrm{V}$$
5		df-fac	$$⊢!=\left\{⟨0,1⟩\right\}\cup seq1\left(\times ,\mathrm{I}\right)$$
6		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
7		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
8	6 7	eqtr3i	$$⊢{\mathbb{Z}}_{\ge 1}={\mathbb{N}}_0\setminus \left\{0\right\}$$
9	8	reseq2i	$$⊢{seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}={seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}$$
10		1z	$$⊢1\in \mathbb{Z}$$
11		seqfn	$$⊢1\in \mathbb{Z}\to seq1\left(\times ,\mathrm{I}\right)Fn{\mathbb{Z}}_{\ge 1}$$
12		fnresdm	$$⊢seq1\left(\times ,\mathrm{I}\right)Fn{\mathbb{Z}}_{\ge 1}\to {seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}=seq1\left(\times ,\mathrm{I}\right)$$
13	10 11 12	mp2b	$$⊢{seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{{\mathbb{Z}}_{\ge 1}}=seq1\left(\times ,\mathrm{I}\right)$$
14	9 13	eqtr3i	$$⊢{seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}=seq1\left(\times ,\mathrm{I}\right)$$
15	14	uneq2i	$$⊢\left\{⟨0,1⟩\right\}\cup \left({seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)=\left\{⟨0,1⟩\right\}\cup seq1\left(\times ,\mathrm{I}\right)$$
16	5 15	eqtr4i	$$⊢!=\left\{⟨0,1⟩\right\}\cup \left({seq1\left(\times ,\mathrm{I}\right)\upharpoonright }_{\left({\mathbb{N}}_0\setminus \left\{0\right\}\right)}\right)$$
17	2 4 16	fvsnun1	$$⊢\top \to 0!=1$$
18	17	mptru	$$⊢0!=1$$