Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-mul01
Next ⟩
sn-subeu
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-mul01
Description:
mul01
without
ax-mulcom
.
(Contributed by
SN
, 5-May-2024)
Ref
Expression
Assertion
sn-mul01
⊢
A
∈
ℂ
→
A
⋅
0
=
0
Proof
Step
Hyp
Ref
Expression
1
id
⊢
A
∈
ℂ
→
A
∈
ℂ
2
0cnd
⊢
A
∈
ℂ
→
0
∈
ℂ
3
1
2
mulcld
⊢
A
∈
ℂ
→
A
⋅
0
∈
ℂ
4
1
2
2
adddid
⊢
A
∈
ℂ
→
A
⁢
0
+
0
=
A
⋅
0
+
A
⋅
0
5
sn-00id
⊢
0
+
0
=
0
6
5
oveq2i
⊢
A
⁢
0
+
0
=
A
⋅
0
7
4
6
eqtr3di
⊢
A
∈
ℂ
→
A
⋅
0
+
A
⋅
0
=
A
⋅
0
8
3
7
sn-addid0
⊢
A
∈
ℂ
→
A
⋅
0
=
0