This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( ! ‘ 𝑁 ) ∈ ℕ )