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 13208

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 11281	. . . 4 ⊢ +∞ ∈ ℝ^*
2		xrltnr 13162	. . . 4 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
3	1, 2	ax-mp 5	. . 3 ⊢ ¬ +∞ < +∞
4		breq1 5117	. . 3 ⊢ (𝐴 = +∞ → (𝐴 < +∞ ↔ +∞ < +∞))
5	3, 4	mtbiri 330	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 < +∞)
6		pnfge 13173	. . . 4 ⊢ (𝐴 ∈ ℝ^* → 𝐴 ≤ +∞)
7		xrleloe 13187	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝐴 ≤ +∞ ↔ (𝐴 < +∞ ∨ 𝐴 = +∞)))
8	1, 7	mpan2 704	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ≤ +∞ ↔ (𝐴 < +∞ ∨ 𝐴 = +∞)))
9	6, 8	mpbid 235	. . 3 ⊢ (𝐴 ∈ ℝ^* → (𝐴 < +∞ ∨ 𝐴 = +∞))
10	9	ord 878	. 2 ⊢ (𝐴 ∈ ℝ^* → (¬ 𝐴 < +∞ → 𝐴 = +∞))
11	5, 10	impbid2 229	1 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∨ wo 861 = wceq 1570 ∈ wcel 2146 class class class wbr 5114 +∞cpnf 11258 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-pre-lttri 11192 ax-pre-lttrn 11193

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-po 5574 df-so 5575 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267

This theorem is used by: xgepnf 13209 xrrebnd 13212 xlt2add 13304 supxrbnd1 13365 supxrbnd2 13366 supxrgtmnf 13373 supxrre2 13375 ioopnfsup 13917 icopnfsup 13918 xrsdsreclblem 21600 ovoliun 25701 ovolicopnf 25720 voliunlem3 25748 volsup 25752 itg2seq 25938 nmoreltpnf 31158 nmopreltpnf 32258 ismblfin 38353 supxrgere 46090 supxrgelem 46094 supxrge 46095 suplesup 46096 nepnfltpnf 46099 xrpnf 46240 sge0repnf 47141 sge0rpcpnf 47176 sge0rernmpt 47177

W3C validator