Theorem fac1

Description: The factorial of 1. (Contributed by NM, 2-Dec-2004) (Revised by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	fac1	⊢ ( ! ‘ 1 ) = 1

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		facnn	⊢ ( 1 ∈ ℕ → ( ! ‘ 1 ) = ( seq 1 ( · , I ) ‘ 1 ) )
3	1 2	ax-mp	⊢ ( ! ‘ 1 ) = ( seq 1 ( · , I ) ‘ 1 )
4		1z	⊢ 1 ∈ ℤ
5		seq1	⊢ ( 1 ∈ ℤ → ( seq 1 ( · , I ) ‘ 1 ) = ( I ‘ 1 ) )
6	4 5	ax-mp	⊢ ( seq 1 ( · , I ) ‘ 1 ) = ( I ‘ 1 )
7		fvi	⊢ ( 1 ∈ ℕ → ( I ‘ 1 ) = 1 )
8	1 7	ax-mp	⊢ ( I ‘ 1 ) = 1
9	3 6 8	3eqtri	⊢ ( ! ‘ 1 ) = 1