Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
sn-negex2
Next ⟩
sn-addcand
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn-negex2
Description:
Proof of
cnegex2
without
ax-mulcom
.
(Contributed by
SN
, 5-May-2024)
Ref
Expression
Assertion
sn-negex2
⊢
A
∈
ℂ
→
∃
b
∈
ℂ
b
+
A
=
0
Proof
Step
Hyp
Ref
Expression
1
sn-negex12
⊢
A
∈
ℂ
→
∃
b
∈
ℂ
A
+
b
=
0
∧
b
+
A
=
0
2
simpr
⊢
A
+
b
=
0
∧
b
+
A
=
0
→
b
+
A
=
0
3
2
reximi
⊢
∃
b
∈
ℂ
A
+
b
=
0
∧
b
+
A
=
0
→
∃
b
∈
ℂ
b
+
A
=
0
4
1
3
syl
⊢
A
∈
ℂ
→
∃
b
∈
ℂ
b
+
A
=
0