Metamath Proof Explorer

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 }↔¬{A}<\mathrm{+\infty }\right)$

Proof

Step Hyp Ref Expression
1 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
2 xrltnr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}\to ¬\mathrm{+\infty }<\mathrm{+\infty }$
3 1 2 ax-mp ${⊢}¬\mathrm{+\infty }<\mathrm{+\infty }$
4 breq1 ${⊢}{A}=\mathrm{+\infty }\to \left({A}<\mathrm{+\infty }↔\mathrm{+\infty }<\mathrm{+\infty }\right)$
5 3 4 mtbiri ${⊢}{A}=\mathrm{+\infty }\to ¬{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 }↔\left({A}<\mathrm{+\infty }\vee {A}=\mathrm{+\infty }\right)\right)$
8 1 7 mpan2 ${⊢}{A}\in {ℝ}^{*}\to \left({A}\le \mathrm{+\infty }↔\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(¬{A}<\mathrm{+\infty }\to {A}=\mathrm{+\infty }\right)$
11 5 10 impbid2 ${⊢}{A}\in {ℝ}^{*}\to \left({A}=\mathrm{+\infty }↔¬{A}<\mathrm{+\infty }\right)$