This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0lepnf

Description: 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion 0lepnf 0 ≤ +∞

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 pnfge ⊢ ( 0 ∈ ℝ* → 0 ≤ +∞ )
3 1 2 ax-mp ⊢ 0 ≤ +∞