Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
recn
Next ⟩
reex
Metamath Proof Explorer
Ascii
Unicode
Theorem
recn
Description:
A real number is a complex number.
(Contributed by
NM
, 10-Aug-1999)
Ref
Expression
Assertion
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
ax-resscn
⊢
ℝ
⊆
ℂ
2
1
sseli
⊢
A
∈
ℝ
→
A
∈
ℂ