Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-addid1
Next ⟩
sn-addcan2d
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-addid1
Description:
addid1
without
ax-mulcom
.
(Contributed by
SN
, 5-May-2024)
Ref
Expression
Assertion
sn-addid1
⊢
A
∈
ℂ
→
A
+
0
=
A
Proof
Step
Hyp
Ref
Expression
1
sn-negex2
⊢
A
∈
ℂ
→
∃
x
∈
ℂ
x
+
A
=
0
2
simprr
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
=
0
3
2
oveq1d
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
+
0
=
0
+
0
4
sn-00id
⊢
0
+
0
=
0
5
3
4
eqtrdi
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
+
0
=
0
6
simprl
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
∈
ℂ
7
simpl
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
A
∈
ℂ
8
0cnd
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
0
∈
ℂ
9
6
7
8
addassd
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
+
0
=
x
+
A
+
0
10
2
5
9
3eqtr2rd
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
+
0
=
x
+
A
11
7
8
addcld
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
A
+
0
∈
ℂ
12
6
11
7
sn-addcand
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
x
+
A
+
0
=
x
+
A
↔
A
+
0
=
A
13
10
12
mpbid
⊢
A
∈
ℂ
∧
x
∈
ℂ
∧
x
+
A
=
0
→
A
+
0
=
A
14
1
13
rexlimddv
⊢
A
∈
ℂ
→
A
+
0
=
A