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

Metamath Proof Explorer

Theorem fac0

Description: The factorial of 0. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion fac0 ⊢ 0 ! = 1

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1 a1i ⊢ ⊤ → 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 3 a1i ⊢ ⊤ → 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 2 4 16 fvsnun1 ⊢ ⊤ → 0 ! = 1
18 17 mptru ⊢ 0 ! = 1