Theorem nltpnft

Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006)

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

Proof

Step	Hyp	Ref	Expression
1		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
2		xrltnr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}\to \neg \mathrm{+\infty }<\mathrm{+\infty }$$
3	1 2	ax-mp	$$⊢\neg \mathrm{+\infty }<\mathrm{+\infty }$$
4		breq1	$$⊢A=\mathrm{+\infty }\to \left(A<\mathrm{+\infty }\leftrightarrow \mathrm{+\infty }<\mathrm{+\infty }\right)$$
5	3 4	mtbiri	$$⊢A=\mathrm{+\infty }\to \neg A<\mathrm{+\infty }$$
6		pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$
7		xrleloe	$$⊢\left(A\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(A\le \mathrm{+\infty }\leftrightarrow \left(A<\mathrm{+\infty }\vee A=\mathrm{+\infty }\right)\right)$$
8	1 7	mpan2	$$⊢A\in {ℝ}^{*}\to \left(A\le \mathrm{+\infty }\leftrightarrow \left(A<\mathrm{+\infty }\vee A=\mathrm{+\infty }\right)\right)$$
9	6 8	mpbid	$$⊢A\in {ℝ}^{*}\to \left(A<\mathrm{+\infty }\vee A=\mathrm{+\infty }\right)$$
10	9	ord	$$⊢A\in {ℝ}^{*}\to \left(\neg A<\mathrm{+\infty }\to A=\mathrm{+\infty }\right)$$
11	5 10	impbid2	$$⊢A\in {ℝ}^{*}\to \left(A=\mathrm{+\infty }\leftrightarrow \neg A<\mathrm{+\infty }\right)$$