Theorem facnn

Description: Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	facnn	$$⊢N\in \mathbb{N}\to N!=seq1\left(\times ,\mathrm{I}\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$$⊢0\in \mathrm{V}$$
2	1	a1i	$$⊢N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)\to 0\in \mathrm{V}$$
3		1ex	$$⊢1\in \mathrm{V}$$
4	3	a1i	$$⊢N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)\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		id	$$⊢N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)\to N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)$$
18	2 4 16 17	fvsnun2	$$⊢N\in \left({\mathbb{N}}_0\setminus \left\{0\right\}\right)\to N!=seq1\left(\times ,\mathrm{I}\right)\left(N\right)$$
19	18 7	eleq2s	$$⊢N\in \mathbb{N}\to N!=seq1\left(\times ,\mathrm{I}\right)\left(N\right)$$