Description: 6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 6t3e18 | ⊢ ( 6 · 3 ) = ; 1 8 |
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 |