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

Theorem xrre 9517
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 706 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  -oo  <  A )
2 ltpnf 9482 . . . . . 6  |-  ( B  e.  RR  ->  B  <  +oo )
32adantl 445 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  B  <  +oo )
4 rexr 8273 . . . . . 6  |-  ( B  e.  RR  ->  B  e.  RR* )
5 pnfxr 9474 . . . . . . 7  |-  +oo  e.  RR*
6 xrlelttr 9506 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  +oo  e.  RR* )  ->  ( ( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo ) )
75, 6mp3an3 1221 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
84, 7sylan2 453 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
93, 8mpan2d 646 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A  <_  B  ->  A  <  +oo ) )
109imp 414 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  A  <_  B
)  ->  A  <  +oo )
1110adantrl 685 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  <  +oo )
12 xrrebnd 9516 . . 3  |-  ( A  e.  RR*  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
1312ad2antrr 695 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
141, 11, 13mpbir2and 847 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 1519   class class class wbr 3582   RRcr 8146    <_ cle 8260    +oocpnf 8261    -oocmnf 8262   RR*cxr 8263    < clt 8264
This theorem is referenced by:  xrrege0  9521  supxrre  9661  infmxrre  9669  caucvglem  10765  pcgcd1  11412  tgioo  16118  ovolunlem1a  16662  ovoliunlem1  16668  ioombl1lem2  16723  itg2monolem2  16913  dvferm1lem  17108  radcnvle  17490  psercnlem1  17495  nmobndi  18669  ubthlem3  18767  nmophmi  19927  bdophsi  19992  bdopcoi  19994
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-13 1523  ax-14 1524  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-sep 3697  ax-nul 3705  ax-pow 3741  ax-pr 3765  ax-un 4057  ax-cnex 8202  ax-resscn 8203  ax-pre-lttri 8220  ax-pre-lttrn 8221
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 894  df-3an 895  df-tru 1256  df-ex 1444  df-sb 1733  df-eu 1955  df-mo 1956  df-clab 2049  df-cleq 2054  df-clel 2057  df-ne 2181  df-nel 2182  df-ral 2275  df-rex 2276  df-rab 2278  df-v 2474  df-sbc 2648  df-csb 2730  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-nul 3070  df-if 3178  df-pw 3239  df-sn 3257  df-pr 3258  df-op 3260  df-uni 3421  df-br 3583  df-opab 3637  df-mpt 3638  df-id 3856  df-po 3861  df-so 3862  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fun 4274  df-fn 4275  df-f 4276  df-f1 4277  df-fo 4278  df-f1o 4279  df-fv 4280  df-er 6107  df-en 6294  df-dom 6295  df-sdom 6296  df-pnf 8265  df-mnf 8266  df-xr 8267  df-ltxr 8268  df-le 8269
Copyright terms: Public domain