Metamath Proof Explorer

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