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