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