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 ) = ( ! ‘ ( 2 + 1 ) )
3		2nn0	⊢ 2 ∈ ℕ0
4		facp1	⊢ ( 2 ∈ ℕ0 → ( ! ‘ ( 2 + 1 ) ) = ( ( ! ‘ 2 ) · ( 2 + 1 ) ) )
5	3 4	ax-mp	⊢ ( ! ‘ ( 2 + 1 ) ) = ( ( ! ‘ 2 ) · ( 2 + 1 ) )
6		fac2	⊢ ( ! ‘ 2 ) = 2
7		2p1e3	⊢ ( 2 + 1 ) = 3
8	6 7	oveq12i	⊢ ( ( ! ‘ 2 ) · ( 2 + 1 ) ) = ( 2 · 3 )
9		2t3e6	⊢ ( 2 · 3 ) = 6
10	8 9	eqtri	⊢ ( ( ! ‘ 2 ) · ( 2 + 1 ) ) = 6
11	2 5 10	3eqtri	⊢ ( ! ‘ 3 ) = 6