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

Metamath Proof Explorer

Theorem fac4

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

		Ref	Expression
	Assertion	fac4	$⊢ 4! = 24$

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