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
Structured
Theorem
recn
Description:
A real number is a complex number.
(Contributed by
NM
, 10-Aug-1999)
Ref
Expression
Assertion
recn
⊢
(
𝐴
∈ ℝ →
𝐴
∈ ℂ )
Proof
Step
Hyp
Ref
Expression
1
ax-resscn
⊢
ℝ ⊆ ℂ
2
1
sseli
⊢
(
𝐴
∈ ℝ →
𝐴
∈ ℂ )