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

Theorem xrre 10316
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 729 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  -oo  <  A )
2 ltpnf 10281 . . . . . 6  |-  ( B  e.  RR  ->  B  <  +oo )
32adantl 448 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  B  <  +oo )
4 rexr 8731 . . . . . 6  |-  ( B  e.  RR  ->  B  e.  RR* )
5 pnfxr 10273 . . . . . . 7  |-  +oo  e.  RR*
6 xrlelttr 10305 . . . . . . 7  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  +oo  e.  RR* )  ->  ( ( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo ) )
75, 6mp3an3 1265 . . . . . 6  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
84, 7sylan2 456 . . . . 5  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  (
( A  <_  B  /\  B  <  +oo )  ->  A  <  +oo )
)
93, 8mpan2d 652 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR )  ->  ( A  <_  B  ->  A  <  +oo ) )
109imp 416 . . 3  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  A  <_  B
)  ->  A  <  +oo )
1110adantrl 693 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  <  +oo )
12 xrrebnd 10315 . . 3  |-  ( A  e.  RR*  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
1312ad2antrr 703 . 2  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  ( A  e.  RR  <->  (  -oo  <  A  /\  A  <  +oo ) ) )
141, 11, 13mpbir2and 887 1  |-  ( ( ( A  e.  RR*  /\  B  e.  RR )  /\  (  -oo  <  A  /\  A  <_  B
) )  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 5    <-> wb 175    /\ wa 357    e. wcel 1610   class class class wbr 3900   RRcr 8590    +oocpnf 8718    -oocmnf 8719   RR*cxr 8720    < clt 8721    <_ cle 8722
This theorem is referenced by:  xrrege0  10320  supxrre  10463  infmxrre  10471  caucvgrlem  11956  pcgcd1  12737  tgioo  17980  ovolunlem1a  18533  ovoliunlem1  18539  ioombl1lem2  18594  itg2monolem2  18784  dvferm1lem  19009  radcnvle  19474  psercnlem1  19479  nmobndi  20984  ubthlem3  21082  nmophmi  22242  bdophsi  22307  bdopcoi  22309
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-13 1614  ax-14 1615  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-sep 4017  ax-nul 4025  ax-pow 4061  ax-pr 4087  ax-un 4382  ax-cnex 8647  ax-resscn 8648  ax-pre-lttri 8665  ax-pre-lttrn 8666
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-3or 934  df-3an 935  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-eu 2106  df-mo 2107  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-ne 2402  df-nel 2403  df-ral 2499  df-rex 2500  df-rab 2502  df-v 2714  df-sbc 2907  df-csb 2990  df-dif 3061  df-un 3063  df-in 3065  df-ss 3069  df-nul 3343  df-if 3451  df-pw 3512  df-sn 3530  df-pr 3531  df-op 3533  df-uni 3708  df-br 3901  df-opab 3955  df-mpt 3956  df-id 4181  df-po 4186  df-so 4187  df-xp 4573  df-rel 4574  df-cnv 4575  df-co 4576  df-dm 4577  df-rn 4578  df-res 4579  df-ima 4580  df-fun 4581  df-fn 4582  df-f 4583  df-f1 4584  df-fo 4585  df-f1o 4586  df-fv 4587  df-er 6520  df-en 6724  df-dom 6725  df-sdom 6726  df-pnf 8723  df-mnf 8724  df-xr 8725  df-ltxr 8726  df-le 8727
  Copyright terms: Public domain W3C validator