Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
4t3e12
Next ⟩
4t4e16
Metamath Proof Explorer
Ascii
Unicode
Theorem
4t3e12
Description:
4 times 3 equals 12.
(Contributed by
Mario Carneiro
, 19-Apr-2015)
Ref
Expression
Assertion
4t3e12
⊢
4
⋅
3
=
12
Proof
Step
Hyp
Ref
Expression
1
4nn0
⊢
4
∈
ℕ
0
2
2nn0
⊢
2
∈
ℕ
0
3
df-3
⊢
3
=
2
+
1
4
4t2e8
⊢
4
⋅
2
=
8
5
8p4e12
⊢
8
+
4
=
12
6
1
2
3
4
5
4t3lem
⊢
4
⋅
3
=
12