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

Theorem xrre 13197
Description: A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
Assertion
Ref Expression
xrre (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)

Proof of Theorem xrre
StepHypRef Expression
1 simprl 769 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → -∞ < 𝐴)
2 ltpnf 13149 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 < +∞)
32adantl 480 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → 𝐵 < +∞)
4 rexr 11306 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
5 pnfxr 11314 . . . . . . 7 +∞ ∈ ℝ*
6 xrlelttr 13184 . . . . . . 7 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝐴𝐵𝐵 < +∞) → 𝐴 < +∞))
75, 6mp3an3 1446 . . . . . 6 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴𝐵𝐵 < +∞) → 𝐴 < +∞))
84, 7sylan2 591 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → ((𝐴𝐵𝐵 < +∞) → 𝐴 < +∞))
93, 8mpan2d 692 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴𝐵𝐴 < +∞))
109imp 405 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ 𝐴𝐵) → 𝐴 < +∞)
1110adantrl 714 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 < +∞)
12 xrrebnd 13196 . . 3 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))
1312ad2antrr 724 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴𝐴 < +∞)))
141, 11, 13mpbir2and 711 1 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ) ∧ (-∞ < 𝐴𝐴𝐵)) → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2098   class class class wbr 5152  cr 11153  +∞cpnf 11291  -∞cmnf 11292  *cxr 11293   < clt 11294  cle 11295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-pre-lttri 11228  ax-pre-lttrn 11229
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-po 5593  df-so 5594  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300
This theorem is referenced by:  xrrege0  13202  supxrre  13355  infxrre  13364  caucvgrlem  15672  pcgcd1  16874  tgioo  24795  ovolunlem1a  25508  ovoliunlem1  25514  ioombl1lem2  25571  itg2monolem2  25764  dvferm1lem  25999  radcnvle  26441  psercnlem1  26447  nmobndi  30700  ubthlem3  30797  nmophmi  31956  bdophsi  32021  bdopcoi  32023  orvclteel  34274  itg2addnclem  37332  itg2gt0cn  37336  areacirclem5  37373  eliocre  45076  fourierdlem87  45763  sge0ssre  45967
  Copyright terms: Public domain W3C validator