# 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\in \mathrm{V}$
2 1 a1i ${⊢}\top \to 0\in \mathrm{V}$
3 1ex ${⊢}1\in \mathrm{V}$
4 3 a1i ${⊢}\top \to 1\in \mathrm{V}$
5 df-fac ${⊢}!=\left\{⟨0,1⟩\right\}\cup seq1\left(×,\mathrm{I}\right)$
6 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
7 dfn2 ${⊢}ℕ={ℕ}_{0}\setminus \left\{0\right\}$
8 6 7 eqtr3i ${⊢}{ℤ}_{\ge 1}={ℕ}_{0}\setminus \left\{0\right\}$
9 8 reseq2i ${⊢}{seq1\left(×,\mathrm{I}\right)↾}_{{ℤ}_{\ge 1}}={seq1\left(×,\mathrm{I}\right)↾}_{\left({ℕ}_{0}\setminus \left\{0\right\}\right)}$
10 1z ${⊢}1\in ℤ$
11 seqfn ${⊢}1\in ℤ\to seq1\left(×,\mathrm{I}\right)Fn{ℤ}_{\ge 1}$
12 fnresdm ${⊢}seq1\left(×,\mathrm{I}\right)Fn{ℤ}_{\ge 1}\to {seq1\left(×,\mathrm{I}\right)↾}_{{ℤ}_{\ge 1}}=seq1\left(×,\mathrm{I}\right)$
13 10 11 12 mp2b ${⊢}{seq1\left(×,\mathrm{I}\right)↾}_{{ℤ}_{\ge 1}}=seq1\left(×,\mathrm{I}\right)$
14 9 13 eqtr3i ${⊢}{seq1\left(×,\mathrm{I}\right)↾}_{\left({ℕ}_{0}\setminus \left\{0\right\}\right)}=seq1\left(×,\mathrm{I}\right)$
15 14 uneq2i ${⊢}\left\{⟨0,1⟩\right\}\cup \left({seq1\left(×,\mathrm{I}\right)↾}_{\left({ℕ}_{0}\setminus \left\{0\right\}\right)}\right)=\left\{⟨0,1⟩\right\}\cup seq1\left(×,\mathrm{I}\right)$
16 5 15 eqtr4i ${⊢}!=\left\{⟨0,1⟩\right\}\cup \left({seq1\left(×,\mathrm{I}\right)↾}_{\left({ℕ}_{0}\setminus \left\{0\right\}\right)}\right)$
17 2 4 16 fvsnun1 ${⊢}\top \to 0!=1$
18 17 mptru ${⊢}0!=1$