HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem xrre 9504
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 711 . 2  |-  ( (
( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  -oo  <  A )
2 ltpnf 9472 . . . . . 6  |-  ( B  e.  RR  ->  B  <  +oo )
32adantl 446 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  B  <  +oo )
4 rexr 8263 . . . . . 6  |-  ( B  e.  RR  ->  B  e.  RR* )
5 pnfxr 9464 . . . . . . 7  |-  +oo  e.  RR*
6 xrlelttr 9493 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  +oo  e.  RR* )  ->  ( ( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo ) )
75, 6mp3an3 1233 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
84, 7sylan2 454 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
93, 8mpan2d 651 . . . 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 690 . 2  |-  ( (
( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  <  +oo )
12 xrrebnd 9503 . . 3  |-  ( A  e.  RR*  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
1312ad2antrr 700 . 2  |-  ( (
( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
141, 11, 13mpbir2and 852 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 357    e. wcel 1538   class class class wbr 3600   RRcr 8136    <_ cle 8250    +oocpnf 8251    -oocmnf 8252   RR*cxr 8253    < clt 8254
This theorem is referenced by:  xrrege0  9508  supxrre  9648  infmxrre  9656  caucvglem  10737  pcgcd1  11384  tgioo  16027  ovolunlem1a  16571  ovoliunlem1  16577  ioombl1lem2  16632  itg2monolem2  16822  dvferm1lem  17017  radcnvle  17399  psercnlem1  17404  nmobndi  18574  ubthlem3  18672  nmophmi  19832  bdophsi  19897  bdopcoi  19899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075  ax-cnex 8192  ax-resscn 8193  ax-pre-lttri 8210  ax-pre-lttrn 8211
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-tru 1268  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-nel 2202  df-ral 2295  df-rex 2296  df-rab 2298  df-v 2494  df-sbc 2668  df-csb 2750  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-op 3281  df-uni 3439  df-br 3601  df-opab 3655  df-mpt 3656  df-id 3874  df-po 3879  df-so 3880  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-er 6102  df-en 6289  df-dom 6290  df-sdom 6291  df-pnf 8255  df-mnf 8256  df-xr 8257  df-ltxr 8258  df-le 8259
Copyright terms: Public domain