Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal arithmetic
7t2e14
Next ⟩
7t3e21
Metamath Proof Explorer
Ascii
Unicode
Theorem
7t2e14
Description:
7 times 2 equals 14.
(Contributed by
Mario Carneiro
, 19-Apr-2015)
Ref
Expression
Assertion
7t2e14
⊢
7
⋅
2
=
14
Proof
Step
Hyp
Ref
Expression
1
7cn
⊢
7
∈
ℂ
2
1
times2i
⊢
7
⋅
2
=
7
+
7
3
7p7e14
⊢
7
+
7
=
14
4
2
3
eqtri
⊢
7
⋅
2
=
14