# Metamath Proof Explorer

## Theorem faccl

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

Ref Expression
Assertion faccl ${⊢}{N}\in {ℕ}_{0}\to {N}!\in ℕ$

### Proof

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