Theorem xgepnf

Description: An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016)

	Ref	Expression
Assertion	xgepnf	$$⊢A\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le A\leftrightarrow A=\mathrm{+\infty }\right)$$

Proof

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