Theorem pnfel0pnf

Description: +oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pnfel0pnf	$$⊢\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		0xr	$$⊢0\in {ℝ}^{*}$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		0lepnf	$$⊢0\le \mathrm{+\infty }$$
4		ubicc2	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$
5	1 2 3 4	mp3an	$$⊢\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$