Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-00idlem3
Next ⟩
sn-00id
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-00idlem3
Description:
Lemma for
sn-00id
.
(Contributed by
SN
, 25-Dec-2023)
Ref
Expression
Assertion
sn-00idlem3
⊢
0
-
ℝ
0
=
1
→
0
+
0
=
0
Proof
Step
Hyp
Ref
Expression
1
oveq2
⊢
0
-
ℝ
0
=
1
→
0
⋅
0
-
ℝ
0
=
0
⋅
1
2
1
oveq1d
⊢
0
-
ℝ
0
=
1
→
0
⋅
0
-
ℝ
0
+
0
=
0
⋅
1
+
0
3
0re
⊢
0
∈
ℝ
4
sn-00idlem1
⊢
0
∈
ℝ
→
0
⋅
0
-
ℝ
0
=
0
-
ℝ
0
5
4
adantr
⊢
0
∈
ℝ
∧
0
∈
ℝ
→
0
⋅
0
-
ℝ
0
=
0
-
ℝ
0
6
5
oveq1d
⊢
0
∈
ℝ
∧
0
∈
ℝ
→
0
⋅
0
-
ℝ
0
+
0
=
0
-
ℝ
0
+
0
7
resubidaddid1
⊢
0
∈
ℝ
∧
0
∈
ℝ
→
0
-
ℝ
0
+
0
=
0
8
6
7
eqtrd
⊢
0
∈
ℝ
∧
0
∈
ℝ
→
0
⋅
0
-
ℝ
0
+
0
=
0
9
3
3
8
mp2an
⊢
0
⋅
0
-
ℝ
0
+
0
=
0
10
9
a1i
⊢
0
-
ℝ
0
=
1
→
0
⋅
0
-
ℝ
0
+
0
=
0
11
ax-1rid
⊢
0
∈
ℝ
→
0
⋅
1
=
0
12
3
11
mp1i
⊢
0
-
ℝ
0
=
1
→
0
⋅
1
=
0
13
12
oveq1d
⊢
0
-
ℝ
0
=
1
→
0
⋅
1
+
0
=
0
+
0
14
2
10
13
3eqtr3rd
⊢
0
-
ℝ
0
=
1
→
0
+
0
=
0