This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ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