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		2cn	⊢ 2 ∈ ℂ
10		3cn	⊢ 3 ∈ ℂ
11	9 10	mulcomi	⊢ ( 2 · 3 ) = ( 3 · 2 )
12		3t2e6	⊢ ( 3 · 2 ) = 6
13	8 11 12	3eqtri	⊢ ( ( ! ‘ 2 ) · ( 2 + 1 ) ) = 6
14	2 5 13	3eqtri	⊢ ( ! ‘ 3 ) = 6