Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Infinity and the extended real number system
rexr
Next ⟩
0xr
Metamath Proof Explorer
Ascii
Structured
Theorem
rexr
Description:
A standard real is an extended real.
(Contributed by
NM
, 14-Oct-2005)
Ref
Expression
Assertion
rexr
⊢
(
𝐴
∈ ℝ →
𝐴
∈ ℝ
*
)
Proof
Step
Hyp
Ref
Expression
1
ressxr
⊢
ℝ ⊆ ℝ
*
2
1
sseli
⊢
(
𝐴
∈ ℝ →
𝐴
∈ ℝ
*
)