nltpnft - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nltpnft		Structured version Visualization version GIF version

Theorem nltpnft 13093

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

**Assertion**
Ref	Expression
nltpnft	⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))

**Proof of Theorem nltpnft**
Step	Hyp	Ref	Expression
1		pnfxr 11218	. . . 4 ⊢ +∞ ∈ ℝ^*
2		xrltnr 13049	. . . 4 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
3	1, 2	ax-mp 5	. . 3 ⊢ ¬ +∞ < +∞
4		breq1 5113	. . 3 ⊢ (𝐴 = +∞ → (𝐴 < +∞ ↔ +∞ < +∞))
5	3, 4	mtbiri 326	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 < +∞)
6		pnfge 13060	. . . 4 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
7		xrleloe 13073	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 ≤ +∞ ↔ (𝐴 < +∞ ∨ 𝐴 = +∞)))
8	1, 7	mpan2 689	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ≤ +∞ ↔ (𝐴 < +∞ ∨ 𝐴 = +∞)))
9	6, 8	mpbid 231	. . 3 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < +∞ ∨ 𝐴 = +∞))
10	9	ord 862	. 2 ⊢ (𝐴 ∈ ℝ^* → (¬ 𝐴 < +∞ → 𝐴 = +∞))
11	5, 10	impbid2 225	1 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 845 = wceq 1541 ∈ wcel 2106 class class class wbr 5110 +∞cpnf 11195 ℝ^*cxr 11197 < clt 11198 ≤ cle 11199

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-cnex 11116 ax-resscn 11117 ax-pre-lttri 11134 ax-pre-lttrn 11135

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204

This theorem is referenced by: xgepnf 13094 xrrebnd 13097 xlt2add 13189 supxrbnd1 13250 supxrbnd2 13251 supxrgtmnf 13258 supxrre2 13260 ioopnfsup 13779 icopnfsup 13780 xrsdsreclblem 20880 ovoliun 24906 ovolicopnf 24925 voliunlem3 24953 volsup 24957 itg2seq 25144 nmoreltpnf 29774 nmopreltpnf 30874 ismblfin 36192 supxrgere 43688 supxrgelem 43692 supxrge 43693 suplesup 43694 nepnfltpnf 43697 xrpnf 43841 sge0repnf 44747 sge0rpcpnf 44782 sge0rernmpt 44783

W3C validator