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\in \mathbb{N}$$
2		facnn	$$⊢1\in \mathbb{N}\to 1!=seq1\left(\times ,\mathrm{I}\right)\left(1\right)$$
3	1 2	ax-mp	$$⊢1!=seq1\left(\times ,\mathrm{I}\right)\left(1\right)$$
4		1z	$$⊢1\in \mathbb{Z}$$
5		seq1	$$⊢1\in \mathbb{Z}\to seq1\left(\times ,\mathrm{I}\right)\left(1\right)=\mathrm{I}\left(1\right)$$
6	4 5	ax-mp	$$⊢seq1\left(\times ,\mathrm{I}\right)\left(1\right)=\mathrm{I}\left(1\right)$$
7		fvi	$$⊢1\in \mathbb{N}\to \mathrm{I}\left(1\right)=1$$
8	1 7	ax-mp	$$⊢\mathrm{I}\left(1\right)=1$$
9	3 6 8	3eqtri	$$⊢1!=1$$