Theorem faccl

Description: Closure of the factorial function. (Contributed by NM, 2-Dec-2004)

	Ref	Expression
Assertion	faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢j=0\to j!=0!$$
2	1	eleq1d	$$⊢j=0\to \left(j!\in \mathbb{N}\leftrightarrow 0!\in \mathbb{N}\right)$$
3		fveq2	$$⊢j=k\to j!=k!$$
4	3	eleq1d	$$⊢j=k\to \left(j!\in \mathbb{N}\leftrightarrow k!\in \mathbb{N}\right)$$
5		fveq2	$$⊢j=k+1\to j!=\left(k+1\right)!$$
6	5	eleq1d	$$⊢j=k+1\to \left(j!\in \mathbb{N}\leftrightarrow \left(k+1\right)!\in \mathbb{N}\right)$$
7		fveq2	$$⊢j=N\to j!=N!$$
8	7	eleq1d	$$⊢j=N\to \left(j!\in \mathbb{N}\leftrightarrow N!\in \mathbb{N}\right)$$
9		fac0	$$⊢0!=1$$
10		1nn	$$⊢1\in \mathbb{N}$$
11	9 10	eqeltri	$$⊢0!\in \mathbb{N}$$
12		facp1	$$⊢k\in {\mathbb{N}}_0\to \left(k+1\right)!=k!\left(k+1\right)$$
13	12	adantl	$$⊢\left(k!\in \mathbb{N}\wedge k\in {\mathbb{N}}_0\right)\to \left(k+1\right)!=k!\left(k+1\right)$$
14		nn0p1nn	$$⊢k\in {\mathbb{N}}_0\to k+1\in \mathbb{N}$$
15		nnmulcl	$$⊢\left(k!\in \mathbb{N}\wedge k+1\in \mathbb{N}\right)\to k!\left(k+1\right)\in \mathbb{N}$$
16	14 15	sylan2	$$⊢\left(k!\in \mathbb{N}\wedge k\in {\mathbb{N}}_0\right)\to k!\left(k+1\right)\in \mathbb{N}$$
17	13 16	eqeltrd	$$⊢\left(k!\in \mathbb{N}\wedge k\in {\mathbb{N}}_0\right)\to \left(k+1\right)!\in \mathbb{N}$$
18	17	expcom	$$⊢k\in {\mathbb{N}}_0\to \left(k!\in \mathbb{N}\to \left(k+1\right)!\in \mathbb{N}\right)$$
19	2 4 6 8 11 18	nn0ind	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$