# 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 e. _V`
2 1 a1i
` |-  ( T. -> 0 e. _V )`
3 1ex
` |-  1 e. _V`
4 3 a1i
` |-  ( T. -> 1 e. _V )`
5 df-fac
` |-  ! = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )`
6 nnuz
` |-  NN = ( ZZ>= ` 1 )`
7 dfn2
` |-  NN = ( NN0 \ { 0 } )`
8 6 7 eqtr3i
` |-  ( ZZ>= ` 1 ) = ( NN0 \ { 0 } )`
9 8 reseq2i
` |-  ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) )`
10 1z
` |-  1 e. ZZ`
11 seqfn
` |-  ( 1 e. ZZ -> seq 1 ( x. , _I ) Fn ( ZZ>= ` 1 ) )`
12 fnresdm
` |-  ( seq 1 ( x. , _I ) Fn ( ZZ>= ` 1 ) -> ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = seq 1 ( x. , _I ) )`
13 10 11 12 mp2b
` |-  ( seq 1 ( x. , _I ) |` ( ZZ>= ` 1 ) ) = seq 1 ( x. , _I )`
14 9 13 eqtr3i
` |-  ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) = seq 1 ( x. , _I )`
15 14 uneq2i
` |-  ( { <. 0 , 1 >. } u. ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) ) = ( { <. 0 , 1 >. } u. seq 1 ( x. , _I ) )`
16 5 15 eqtr4i
` |-  ! = ( { <. 0 , 1 >. } u. ( seq 1 ( x. , _I ) |` ( NN0 \ { 0 } ) ) )`
17 2 4 16 fvsnun1
` |-  ( T. -> ( ! ` 0 ) = 1 )`
18 17 mptru
` |-  ( ! ` 0 ) = 1`