Theorem fac4

Description: The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Assertion	fac4	$$⊢4!=24$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		facp1	$$⊢3\in {\mathbb{N}}_0\to \left(3+1\right)!=3!\left(3+1\right)$$
3	1 2	ax-mp	$$⊢\left(3+1\right)!=3!\left(3+1\right)$$
4		3p1e4	$$⊢3+1=4$$
5	4	fveq2i	$$⊢\left(3+1\right)!=4!$$
6		fac3	$$⊢3!=6$$
7	6 4	oveq12i	$$⊢3!\left(3+1\right)=6\cdot 4$$
8		6t4e24	$$⊢6\cdot 4=24$$
9	7 8	eqtri	$$⊢3!\left(3+1\right)=24$$
10	3 5 9	3eqtr3i	$$⊢4!=24$$