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 ⊢ N ∈ ℕ 0 → N ! ∈ ℕ

Proof

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