Theorem pnfge

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006)

	Ref	Expression
Assertion	pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		pnfnlt	$$⊢A\in {ℝ}^{*}\to \neg \mathrm{+\infty }<A$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		xrlenlt	$$⊢\left(A\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(A\le \mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }<A\right)$$
4	2 3	mpan2	$$⊢A\in {ℝ}^{*}\to \left(A\le \mathrm{+\infty }\leftrightarrow \neg \mathrm{+\infty }<A\right)$$
5	1 4	mpbird	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$