This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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$

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		facnn	$⊢ 1 \in ℕ \to 1! = seq 1 (\times I) (1)$
3	1 2	ax-mp	$⊢ 1! = seq 1 (\times I) (1)$
4		1z	$⊢ 1 \in ℤ$
5		seq1	$⊢ 1 \in ℤ \to seq 1 (\times I) (1) = I (1)$
6	4 5	ax-mp	$⊢ seq 1 (\times I) (1) = I (1)$
7		fvi	$⊢ 1 \in ℕ \to I (1) = 1$
8	1 7	ax-mp	$⊢ I (1) = 1$
9	3 6 8	3eqtri	$⊢ 1! = 1$