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