Theorem faccl

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

	Ref	Expression
Assertion	faccl	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑗 = 0 → ( ! ‘ 𝑗 ) = ( ! ‘ 0 ) )
2	1	eleq1d	⊢ ( 𝑗 = 0 → ( ( ! ‘ 𝑗 ) ∈ ℕ ↔ ( ! ‘ 0 ) ∈ ℕ ) )
3		fveq2	⊢ ( 𝑗 = 𝑘 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑘 ) )
4	3	eleq1d	⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑗 ) ∈ ℕ ↔ ( ! ‘ 𝑘 ) ∈ ℕ ) )
5		fveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( 𝑘 + 1 ) ) )
6	5	eleq1d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑗 ) ∈ ℕ ↔ ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) )
7		fveq2	⊢ ( 𝑗 = 𝑁 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑁 ) )
8	7	eleq1d	⊢ ( 𝑗 = 𝑁 → ( ( ! ‘ 𝑗 ) ∈ ℕ ↔ ( ! ‘ 𝑁 ) ∈ ℕ ) )
9		fac0	⊢ ( ! ‘ 0 ) = 1
10		1nn	⊢ 1 ∈ ℕ
11	9 10	eqeltri	⊢ ( ! ‘ 0 ) ∈ ℕ
12		facp1	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
13	12	adantl	⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) )
14		nn0p1nn	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ )
15		nnmulcl	⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ∈ ℕ )
16	14 15	sylan2	⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ∈ ℕ )
17	13 16	eqeltrd	⊢ ( ( ( ! ‘ 𝑘 ) ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℕ )
18	17	expcom	⊢ ( 𝑘 ∈ ℕ0 → ( ( ! ‘ 𝑘 ) ∈ ℕ → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) )
19	2 4 6 8 11 18	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )