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
Structured
Theorem
recni
Description:
A real number is a complex number.
(Contributed by
NM
, 1-Mar-1995)
Ref
Expression
Hypothesis
recni.1
⊢
𝐴
∈ ℝ
Assertion
recni
⊢
𝐴
∈ ℂ
Proof
Step
Hyp
Ref
Expression
1
recni.1
⊢
𝐴
∈ ℝ
2
ax-resscn
⊢
ℝ ⊆ ℂ
3
2
1
sselii
⊢
𝐴
∈ ℂ