Theorem fac3

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

	Ref	Expression
Assertion	fac3	$$⊢3!=6$$

Proof

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