Database
REAL AND COMPLEX NUMBERS
Order sets
Infinity and the extended real number system (cont.)
mnflt0
Next ⟩
mnfltpnf
Metamath Proof Explorer
Ascii
Structured
Theorem
mnflt0
Description:
Minus infinity is less than 0.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
mnflt0
⊢
-∞ < 0
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0 ∈ ℝ
2
mnflt
⊢
( 0 ∈ ℝ → -∞ < 0 )
3
1
2
ax-mp
⊢
-∞ < 0