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