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