Theorem fac2

Description: The factorial of 2. (Contributed by NM, 17-Mar-2005)

	Ref	Expression
Assertion	fac2	$$⊢2!=2$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	fveq2i	$$⊢2!=\left(1+1\right)!$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4		facp1	$$⊢1\in {\mathbb{N}}_0\to \left(1+1\right)!=1!\left(1+1\right)$$
5	3 4	ax-mp	$$⊢\left(1+1\right)!=1!\left(1+1\right)$$
6		fac1	$$⊢1!=1$$
7		1p1e2	$$⊢1+1=2$$
8	6 7	oveq12i	$$⊢1!\left(1+1\right)=1\cdot 2$$
9		2cn	$$⊢2\in ℂ$$
10	9	mulid2i	$$⊢1\cdot 2=2$$
11	8 10	eqtri	$$⊢1!\left(1+1\right)=2$$
12	5 11	eqtri	$$⊢\left(1+1\right)!=2$$
13	2 12	eqtri	$$⊢2!=2$$