Metamath Proof Explorer


Theorem 6t3e18

Description: 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 6t3e18 ( 6 · 3 ) = 1 8

Proof

Step Hyp Ref Expression
1 6nn0 6 ∈ ℕ0
2 2nn0 2 ∈ ℕ0
3 df-3 3 = ( 2 + 1 )
4 6t2e12 ( 6 · 2 ) = 1 2
5 1nn0 1 ∈ ℕ0
6 eqid 1 2 = 1 2
7 6cn 6 ∈ ℂ
8 2cn 2 ∈ ℂ
9 6p2e8 ( 6 + 2 ) = 8
10 7 8 9 addcomli ( 2 + 6 ) = 8
11 5 2 1 6 10 decaddi ( 1 2 + 6 ) = 1 8
12 1 2 3 4 11 4t3lem ( 6 · 3 ) = 1 8