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

Theorem xrre 8190
Description: A way of proving that an extended real is real.
Assertion
Ref Expression
xrre |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> A e. RR)

Proof of Theorem xrre
StepHypRef Expression
1 xrrebnd 8189 . . 3 |- (A e. RR* -> (A e. RR <-> ( -oo < A /\ A < +oo)))
21ad2antrr 726 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> (A e. RR <-> ( -oo < A /\ A < +oo)))
3 simprl 737 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> -oo < A)
4 ltpnf 8162 . . . . . 6 |- (B e. RR -> B < +oo)
54adantl 469 . . . . 5 |- ((A e. RR* /\ B e. RR) -> B < +oo)
6 rexr 7119 . . . . . 6 |- (B e. RR -> B e. RR*)
7 pnfxr 8156 . . . . . . 7 |- +oo e. RR*
8 xrlelttr 8183 . . . . . . 7 |- ((A e. RR* /\ B e. RR* /\ +oo e. RR*) -> ((A <_ B /\ B < +oo) -> A < +oo))
97, 8mp3an3 1262 . . . . . 6 |- ((A e. RR* /\ B e. RR*) -> ((A <_ B /\ B < +oo) -> A < +oo))
106, 9sylan2 477 . . . . 5 |- ((A e. RR* /\ B e. RR) -> ((A <_ B /\ B < +oo) -> A < +oo))
115, 10mpan2d 672 . . . 4 |- ((A e. RR* /\ B e. RR) -> (A <_ B -> A < +oo))
1211imp 437 . . 3 |- (((A e. RR* /\ B e. RR) /\ A <_ B) -> A < +oo)
1312adantrl 716 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> A < +oo)
142, 3, 13mpbir2and 889 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 184   /\ wa 377   e. wcel 1451   class class class wbr 3373  RRcr 6997   <_ cle 7106   +oocpnf 7107   -oocmnf 7108  RR*cxr 7109   < clt 7110
This theorem is referenced by:  supxrre 8237  infmxrre 8244  caucvglem 9188  tgioo 11350  nmobndi 11790  ubthlem3 11888  ovollecl 12000  ovolunlem1 12012  ovoliunlem1 12016  ioombl1lem2 12065  itg2lecl 12210  itg2monolem2 12223  nmophmi 13876  bdophsi 13941  bdopcoi 13943  elioc3 15582
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808  ax-inf2 6071  ax-resscn 7052  ax-1cn 7053  ax-icn 7054  ax-addcl 7055  ax-addrcl 7056  ax-mulcl 7057  ax-mulrcl 7058  ax-mulcom 7059  ax-addass 7060  ax-mulass 7061  ax-distr 7062  ax-i2m1 7063  ax-1ne0 7064  ax-1rid 7065  ax-rnegex 7066  ax-rrecex 7067  ax-cnre 7068  ax-pre-lttri 7069  ax-pre-lttrn 7070  ax-pre-ltadd 7071  ax-pre-mulgt0 7072  ax-pre-sup 7073
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-tru 1345  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-nel 2074  df-ral 2166  df-rex 2167  df-reu 2168  df-rab 2169  df-v 2360  df-sbc 2525  df-csb 2600  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-if 3023  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-iun 3301  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3971  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-f1 4029  df-fo 4030  df-f1o 4031  df-fv 4032  df-ov 4933  df-oprab 4934  df-mpt 5068  df-mpt2 5069  df-1st 5166  df-2nd 5167  df-iota 5270  df-rdg 5356  df-er 5530  df-map 5618  df-en 5675  df-dom 5676  df-sdom 5677  df-riota 5818  df-sup 5992  df-pnf 7111  df-mnf 7112  df-xr 7113  df-ltxr 7114  df-le 7115  df-sub 7240  df-neg 7242  df-div 7466  df-n 7704  df-n0 7874  df-z 7918  df-uz 8038  df-q 8120
Copyright terms: Public domain