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