Theorem fac2

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

	Ref	Expression
Assertion	fac2	⊢ ( ! ‘ 2 ) = 2

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	fveq2i	⊢ ( ! ‘ 2 ) = ( ! ‘ ( 1 + 1 ) )
3		1nn0	⊢ 1 ∈ ℕ0
4		facp1	⊢ ( 1 ∈ ℕ0 → ( ! ‘ ( 1 + 1 ) ) = ( ( ! ‘ 1 ) · ( 1 + 1 ) ) )
5	3 4	ax-mp	⊢ ( ! ‘ ( 1 + 1 ) ) = ( ( ! ‘ 1 ) · ( 1 + 1 ) )
6		fac1	⊢ ( ! ‘ 1 ) = 1
7		1p1e2	⊢ ( 1 + 1 ) = 2
8	6 7	oveq12i	⊢ ( ( ! ‘ 1 ) · ( 1 + 1 ) ) = ( 1 · 2 )
9		2cn	⊢ 2 ∈ ℂ
10	9	mulid2i	⊢ ( 1 · 2 ) = 2
11	8 10	eqtri	⊢ ( ( ! ‘ 1 ) · ( 1 + 1 ) ) = 2
12	5 11	eqtri	⊢ ( ! ‘ ( 1 + 1 ) ) = 2
13	2 12	eqtri	⊢ ( ! ‘ 2 ) = 2