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+∞