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

Theorem xrre 9867
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 708 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  -oo  <  A )
2 ltpnf 9832 . . . . . 6  |-  ( B  e.  RR  ->  B  <  +oo )
32adantl 446 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  B  <  +oo )
4 rexr 8295 . . . . . 6  |-  ( B  e.  RR  ->  B  e.  RR* )
5 pnfxr 9824 . . . . . . 7  |-  +oo  e.  RR*
6 xrlelttr 9856 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  +oo  e.  RR* )  ->  ( ( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo ) )
75, 6mp3an3 1224 . . . . . 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 648 . . . 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 687 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  <  +oo )
12 xrrebnd 9866 . . 3  |-  ( A  e.  RR*  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
1312ad2antrr 697 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
141, 11, 13mpbir2and 850 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 1522   class class class wbr 3586   RRcr 8157    <_ cle 8282    +oocpnf 8283    -oocmnf 8284   RR*cxr 8285    < clt 8286
This theorem is referenced by:  xrrege0  9871  supxrre  10014  infmxrre  10022  caucvgrlem  11336  pcgcd1  12034  tgioo  16990  ovolunlem1a  17535  ovoliunlem1  17541  ioombl1lem2  17596  itg2monolem2  17786  dvferm1lem  17985  radcnvle  18384  psercnlem1  18389  nmobndi  19886  ubthlem3  19984  nmophmi  21144  bdophsi  21209  bdopcoi  21211
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-13 1526  ax-14 1527  ax-17 1529  ax-12o 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-sep 3701  ax-nul 3709  ax-pow 3745  ax-pr 3769  ax-un 4061  ax-cnex 8213  ax-resscn 8214  ax-pre-lttri 8231  ax-pre-lttrn 8232
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 897  df-3an 898  df-tru 1259  df-ex 1447  df-sb 1736  df-eu 1958  df-mo 1959  df-clab 2052  df-cleq 2057  df-clel 2060  df-ne 2184  df-nel 2185  df-ral 2278  df-rex 2279  df-rab 2281  df-v 2477  df-sbc 2651  df-csb 2733  df-dif 2796  df-un 2798  df-in 2800  df-ss 2804  df-nul 3073  df-if 3182  df-pw 3243  df-sn 3261  df-pr 3262  df-op 3264  df-uni 3425  df-br 3587  df-opab 3641  df-mpt 3642  df-id 3860  df-po 3865  df-so 3866  df-xp 4270  df-rel 4271  df-cnv 4272  df-co 4273  df-dm 4274  df-rn 4275  df-res 4276  df-ima 4277  df-fun 4278  df-fn 4279  df-f 4280  df-f1 4281  df-fo 4282  df-f1o 4283  df-fv 4284  df-er 6115  df-en 6302  df-dom 6303  df-sdom 6304  df-pnf 8287  df-mnf 8288  df-xr 8289  df-ltxr 8290  df-le 8291
Copyright terms: Public domain