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

Theorem xrrebnd 12190
Description: An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
Assertion
Ref Expression
xrrebnd (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))

Proof of Theorem xrrebnd
StepHypRef Expression
1 mnflt 12148 . . 3 (𝐴 ∈ ℝ → -∞ < 𝐴)
2 ltpnf 12145 . . 3 (𝐴 ∈ ℝ → 𝐴 < +∞)
31, 2jca 555 . 2 (𝐴 ∈ ℝ → (-∞ < 𝐴𝐴 < +∞))
4 nltpnft 12186 . . . . . 6 (𝐴 ∈ ℝ* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
5 ngtmnft 12188 . . . . . 6 (𝐴 ∈ ℝ* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
64, 5orbi12d 748 . . . . 5 (𝐴 ∈ ℝ* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴)))
7 ianor 510 . . . . . 6 (¬ (-∞ < 𝐴𝐴 < +∞) ↔ (¬ -∞ < 𝐴 ∨ ¬ 𝐴 < +∞))
8 orcom 401 . . . . . 6 ((¬ -∞ < 𝐴 ∨ ¬ 𝐴 < +∞) ↔ (¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴))
97, 8bitr2i 265 . . . . 5 ((¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴) ↔ ¬ (-∞ < 𝐴𝐴 < +∞))
106, 9syl6bb 276 . . . 4 (𝐴 ∈ ℝ* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ↔ ¬ (-∞ < 𝐴𝐴 < +∞)))
1110con2bid 343 . . 3 (𝐴 ∈ ℝ* → ((-∞ < 𝐴𝐴 < +∞) ↔ ¬ (𝐴 = +∞ ∨ 𝐴 = -∞)))
12 elxr 12141 . . . . 5 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
13 3orass 1075 . . . . . 6 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
14 orcom 401 . . . . . 6 ((𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)) ↔ ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
1513, 14bitri 264 . . . . 5 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
1612, 15sylbb 209 . . . 4 (𝐴 ∈ ℝ* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
1716ord 391 . . 3 (𝐴 ∈ ℝ* → (¬ (𝐴 = +∞ ∨ 𝐴 = -∞) → 𝐴 ∈ ℝ))
1811, 17sylbid 230 . 2 (𝐴 ∈ ℝ* → ((-∞ < 𝐴𝐴 < +∞) → 𝐴 ∈ ℝ))
193, 18impbid2 216 1 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1071   = wceq 1630  wcel 2137   class class class wbr 4802  cr 10125  +∞cpnf 10261  -∞cmnf 10262  *cxr 10263   < clt 10264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-pre-lttri 10200  ax-pre-lttrn 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270
This theorem is referenced by:  xrre  12191  xrre2  12192  xrre3  12193  supxrre1  12351  elioc2  12427  elico2  12428  elicc2  12429  xblpnfps  22399  xblpnf  22400  isnghm3  22728  ovoliun  23471  ovolicopnf  23490  voliunlem3  23518  volsup  23522  itg2seq  23706  nmblore  27948  nmopre  29036  supxrgere  40045  supxrgelem  40049  supxrge  40050  suplesup  40051  infrpge  40063  limsupre  40374
  Copyright terms: Public domain W3C validator