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

Theorem xrre 9920
Description: A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
Assertion
Ref Expression
xrre  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  e.  RR )

Proof of Theorem xrre
StepHypRef Expression
1 simprl 712 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  -oo  <  A )
2 ltpnf 9885 . . . . . 6  |-  ( B  e.  RR  ->  B  <  +oo )
32adantl 447 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  B  <  +oo )
4 rexr 8341 . . . . . 6  |-  ( B  e.  RR  ->  B  e.  RR* )
5 pnfxr 9877 . . . . . . 7  |-  +oo  e.  RR*
6 xrlelttr 9909 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  +oo  e.  RR* )  ->  ( ( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo ) )
75, 6mp3an3 1230 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
84, 7sylan2 455 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
93, 8mpan2d 650 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A  <_  B  ->  A  <  +oo ) )
109imp 415 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  A  <_  B
)  ->  A  <  +oo )
1110adantrl 691 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  <  +oo )
12 xrrebnd 9919 . . 3  |-  ( A  e.  RR*  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
1312ad2antrr 701 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
141, 11, 13mpbir2and 854 1  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 174    /\ wa 356    e. wcel 1533   class class class wbr 3630   RRcr 8201    <_ cle 8328    +oocpnf 8329    -oocmnf 8330   RR*cxr 8331    < clt 8332
This theorem is referenced by:  xrrege0  9924  supxrre  10067  infmxrre  10075  caucvgrlem  11390  pcgcd1  12088  tgioo  17045  ovolunlem1a  17590  ovoliunlem1  17596  ioombl1lem2  17651  itg2monolem2  17841  dvferm1lem  18040  radcnvle  18439  psercnlem1  18444  nmobndi  19943  ubthlem3  20041  nmophmi  21201  bdophsi  21266  bdopcoi  21268
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-13 1537  ax-14 1538  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745  ax-nul 3753  ax-pow 3789  ax-pr 3813  ax-un 4105  ax-cnex 8257  ax-resscn 8258  ax-pre-lttri 8275  ax-pre-lttrn 8276
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 901  df-3an 902  df-tru 1265  df-ex 1457  df-sb 1748  df-eu 1970  df-mo 1971  df-clab 2088  df-cleq 2093  df-clel 2096  df-ne 2220  df-nel 2221  df-ral 2315  df-rex 2316  df-rab 2318  df-v 2514  df-sbc 2688  df-csb 2770  df-dif 2833  df-un 2835  df-in 2837  df-ss 2841  df-nul 3111  df-if 3221  df-pw 3282  df-sn 3300  df-pr 3301  df-op 3303  df-uni 3469  df-br 3631  df-opab 3685  df-mpt 3686  df-id 3904  df-po 3909  df-so 3910  df-xp 4314  df-rel 4315  df-cnv 4316  df-co 4317  df-dm 4318  df-rn 4319  df-res 4320  df-ima 4321  df-fun 4322  df-fn 4323  df-f 4324  df-f1 4325  df-fo 4326  df-f1o 4327  df-fv 4328  df-er 6159  df-en 6346  df-dom 6347  df-sdom 6348  df-pnf 8333  df-mnf 8334  df-xr 8335  df-ltxr 8336  df-le 8337
  Copyright terms: Public domain W3C validator