Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Infinity and the extended real number system
1xr
Next ⟩
renfdisj
Metamath Proof Explorer
Ascii
Structured
Theorem
1xr
Description:
1
is an extended real number.
(Contributed by
Glauco Siliprandi
, 2-Jan-2022)
Ref
Expression
Assertion
1xr
⊢
1 ∈ ℝ
^{*}
Proof
Step
Hyp
Ref
Expression
1
1re
⊢
1 ∈ ℝ
2
1
rexri
⊢
1 ∈ ℝ
^{*}