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
Unicode
Theorem
rexr
Description:
A standard real is an extended real.
(Contributed by
NM
, 14-Oct-2005)
Ref
Expression
Assertion
rexr
⊢
A
∈
ℝ
→
A
∈
ℝ
*
Proof
Step
Hyp
Ref
Expression
1
ressxr
⊢
ℝ
⊆
ℝ
*
2
1
sseli
⊢
A
∈
ℝ
→
A
∈
ℝ
*