Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
cnre
Next ⟩
mulid1
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnre
Description:
Alias for
ax-cnre
, for naming consistency.
(Contributed by
NM
, 3-Jan-2013)
Ref
Expression
Assertion
cnre
⊢
A
∈
ℂ
→
∃
x
∈
ℝ
∃
y
∈
ℝ
A
=
x
+
i
⁢
y
Proof
Step
Hyp
Ref
Expression
1
ax-cnre
⊢
A
∈
ℂ
→
∃
x
∈
ℝ
∃
y
∈
ℝ
A
=
x
+
i
⁢
y