Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
recni
Next ⟩
readdcli
Metamath Proof Explorer
Ascii
Unicode
Theorem
recni
Description:
A real number is a complex number.
(Contributed by
NM
, 1-Mar-1995)
Ref
Expression
Hypothesis
recni.1
⊢
A
∈
ℝ
Assertion
recni
⊢
A
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
recni.1
⊢
A
∈
ℝ
2
ax-resscn
⊢
ℝ
⊆
ℂ
3
2
1
sselii
⊢
A
∈
ℂ