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