Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Infinity and the extended real number system
0xr
Next ⟩
renepnf
Metamath Proof Explorer
Ascii
Unicode
Theorem
0xr
Description:
Zero is an extended real.
(Contributed by
Mario Carneiro
, 15-Jun-2014)
Ref
Expression
Assertion
0xr
⊢
0
∈
ℝ
*
Proof
Step
Hyp
Ref
Expression
1
ressxr
⊢
ℝ
⊆
ℝ
*
2
0re
⊢
0
∈
ℝ
3
1
2
sselii
⊢
0
∈
ℝ
*