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 e. NN0
4		facp1	|- ( 1 e. NN0 -> ( ! ` ( 1 + 1 ) ) = ( ( ! ` 1 ) x. ( 1 + 1 ) ) )
5	3 4	ax-mp	|- ( ! ` ( 1 + 1 ) ) = ( ( ! ` 1 ) x. ( 1 + 1 ) )
6		fac1	|- ( ! ` 1 ) = 1
7		1p1e2	|- ( 1 + 1 ) = 2
8	6 7	oveq12i	|- ( ( ! ` 1 ) x. ( 1 + 1 ) ) = ( 1 x. 2 )
9		2cn	|- 2 e. CC
10	9	mullidi	|- ( 1 x. 2 ) = 2
11	8 10	eqtri	|- ( ( ! ` 1 ) x. ( 1 + 1 ) ) = 2
12	5 11	eqtri	|- ( ! ` ( 1 + 1 ) ) = 2
13	2 12	eqtri	|- ( ! ` 2 ) = 2