Metamath Proof Explorer

Theorem facnn

Description: Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion facnn ⊢ N ∈ ℕ → N ! = seq 1 × I ⁡ N

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1 a1i ⊢ N ∈ ℕ 0 ∖ 0 → 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 3 a1i ⊢ N ∈ ℕ 0 ∖ 0 → 1 ∈ V
5 df-fac ⊢ ! = 0 1 ∪ seq 1 × I
6 nnuz ⊢ ℕ = ℤ ≥ 1
7 dfn2 ⊢ ℕ = ℕ 0 ∖ 0
8 6 7 eqtr3i ⊢ ℤ ≥ 1 = ℕ 0 ∖ 0
9 8 reseq2i ⊢ seq 1 × I ↾ ℤ ≥ 1 = seq 1 × I ↾ ℕ 0 ∖ 0
10 1z ⊢ 1 ∈ ℤ
11 seqfn ⊢ 1 ∈ ℤ → seq 1 × I Fn ℤ ≥ 1
12 fnresdm ⊢ seq 1 × I Fn ℤ ≥ 1 → seq 1 × I ↾ ℤ ≥ 1 = seq 1 × I
13 10 11 12 mp2b ⊢ seq 1 × I ↾ ℤ ≥ 1 = seq 1 × I
14 9 13 eqtr3i ⊢ seq 1 × I ↾ ℕ 0 ∖ 0 = seq 1 × I
15 14 uneq2i ⊢ 0 1 ∪ seq 1 × I ↾ ℕ 0 ∖ 0 = 0 1 ∪ seq 1 × I
16 5 15 eqtr4i ⊢ ! = 0 1 ∪ seq 1 × I ↾ ℕ 0 ∖ 0
17 id ⊢ N ∈ ℕ 0 ∖ 0 → N ∈ ℕ 0 ∖ 0
18 2 4 16 17 fvsnun2 ⊢ N ∈ ℕ 0 ∖ 0 → N ! = seq 1 × I ⁡ N
19 18 7 eleq2s ⊢ N ∈ ℕ → N ! = seq 1 × I ⁡ N