Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
renegid2
Next ⟩
sn-it0e0
Metamath Proof Explorer
Ascii
Unicode
Theorem
renegid2
Description:
Commuted version of
renegid
.
(Contributed by
SN
, 4-May-2024)
Ref
Expression
Assertion
renegid2
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
=
0
Proof
Step
Hyp
Ref
Expression
1
renegid
⊢
A
∈
ℝ
→
A
+
0
-
ℝ
A
=
0
2
1
oveq2d
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
-
ℝ
A
+
0
3
rernegcl
⊢
A
∈
ℝ
→
0
-
ℝ
A
∈
ℝ
4
readdid1
⊢
0
-
ℝ
A
∈
ℝ
→
0
-
ℝ
A
+
0
=
0
-
ℝ
A
5
3
4
syl
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
0
=
0
-
ℝ
A
6
2
5
eqtrd
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
-
ℝ
A
7
3
recnd
⊢
A
∈
ℝ
→
0
-
ℝ
A
∈
ℂ
8
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
9
7
8
7
addassd
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
-
ℝ
A
+
A
+
0
-
ℝ
A
10
readdid2
⊢
0
-
ℝ
A
∈
ℝ
→
0
+
0
-
ℝ
A
=
0
-
ℝ
A
11
3
10
syl
⊢
A
∈
ℝ
→
0
+
0
-
ℝ
A
=
0
-
ℝ
A
12
6
9
11
3eqtr4d
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
+
0
-
ℝ
A
13
id
⊢
A
∈
ℝ
→
A
∈
ℝ
14
3
13
readdcld
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
∈
ℝ
15
elre0re
⊢
A
∈
ℝ
→
0
∈
ℝ
16
readdcan2
⊢
0
-
ℝ
A
+
A
∈
ℝ
∧
0
∈
ℝ
∧
0
-
ℝ
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
+
0
-
ℝ
A
↔
0
-
ℝ
A
+
A
=
0
17
14
15
3
16
syl3anc
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
+
0
-
ℝ
A
=
0
+
0
-
ℝ
A
↔
0
-
ℝ
A
+
A
=
0
18
12
17
mpbid
⊢
A
∈
ℝ
→
0
-
ℝ
A
+
A
=
0