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

Theorem xrre 8177
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 8176 . . 3 |- (A e. RR* -> (A e. RR <-> ( -oo < A /\ A < +oo)))
21ad2antrr 706 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> (A e. RR <-> ( -oo < A /\ A < +oo)))
3 simprl 717 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> -oo < A)
4 ltpnf 8149 . . . . . 6 |- (B e. RR -> B < +oo)
54adantl 449 . . . . 5 |- ((A e. RR* /\ B e. RR) -> B < +oo)
6 rexr 7105 . . . . . 6 |- (B e. RR -> B e. RR*)
7 pnfxr 8143 . . . . . . 7 |- +oo e. RR*
8 xrlelttr 8170 . . . . . . 7 |- ((A e. RR* /\ B e. RR* /\ +oo e. RR*) -> ((A <_ B /\ B < +oo) -> A < +oo))
97, 8mp3an3 1240 . . . . . 6 |- ((A e. RR* /\ B e. RR*) -> ((A <_ B /\ B < +oo) -> A < +oo))
106, 9sylan2 457 . . . . 5 |- ((A e. RR* /\ B e. RR) -> ((A <_ B /\ B < +oo) -> A < +oo))
115, 10mpan2d 652 . . . 4 |- ((A e. RR* /\ B e. RR) -> (A <_ B -> A < +oo))
1211imp 417 . . 3 |- (((A e. RR* /\ B e. RR) /\ A <_ B) -> A < +oo)
1312adantrl 696 . 2 |- (((A e. RR* /\ B e. RR) /\ ( -oo < A /\ A <_ B)) -> A < +oo)
142, 3, 13mpbir2and 868 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 1430   class class class wbr 3354  RRcr 6983   <_ cle 7092   +oocpnf 7093   -oocmnf 7094  RR*cxr 7095   < clt 7096
This theorem is referenced by:  supxrre 8224  infmxrre 8231  caucvglem 9229  tgioo 11436  nmobndi 11875  ubthlem3 11973  ovollecl 12087  ovolunlem1 12099  ovoliunlem1 12103  ioombl1lem2 12152  itg2lecl 12297  itg2monolem2 12310  nmophmi 14062  bdophsi 14127  bdopcoi 14129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-13 1436  ax-14 1437  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914  ax-rep 3440  ax-sep 3450  ax-nul 3459  ax-pow 3495  ax-pr 3519  ax-un 3791  ax-inf2 6055  ax-resscn 7038  ax-1cn 7039  ax-icn 7040  ax-addcl 7041  ax-addrcl 7042  ax-mulcl 7043  ax-mulrcl 7044  ax-mulcom 7045  ax-addass 7046  ax-mulass 7047  ax-distr 7048  ax-i2m1 7049  ax-1ne0 7050  ax-1rid 7051  ax-rnegex 7052  ax-rrecex 7053  ax-cnre 7054  ax-pre-lttri 7055  ax-pre-lttrn 7056  ax-pre-ltadd 7057  ax-pre-mulgt0 7058  ax-pre-sup 7059
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 916  df-3an 917  df-tru 1323  df-ex 1350  df-sb 1605  df-eu 1832  df-mo 1833  df-clab 1920  df-cleq 1925  df-clel 1928  df-ne 2052  df-nel 2053  df-ral 2145  df-rex 2146  df-reu 2147  df-rab 2148  df-v 2339  df-sbc 2504  df-csb 2579  df-dif 2639  df-un 2641  df-in 2643  df-ss 2645  df-pss 2647  df-nul 2901  df-if 3002  df-pw 3060  df-sn 3077  df-pr 3078  df-tp 3079  df-op 3080  df-uni 3210  df-iun 3282  df-br 3355  df-opab 3409  df-tr 3424  df-eprel 3604  df-id 3607  df-po 3612  df-so 3626  df-fr 3645  df-we 3661  df-ord 3677  df-on 3678  df-lim 3679  df-suc 3680  df-om 3954  df-xp 4001  df-rel 4002  df-cnv 4003  df-co 4004  df-dm 4005  df-rn 4006  df-res 4007  df-ima 4008  df-fun 4009  df-fn 4010  df-f 4011  df-f1 4012  df-fo 4013  df-f1o 4014  df-fv 4015  df-ov 4916  df-oprab 4917  df-mpt 5051  df-mpt2 5052  df-1st 5150  df-2nd 5151  df-iota 5254  df-rdg 5340  df-er 5514  df-map 5602  df-en 5659  df-dom 5660  df-sdom 5661  df-riota 5802  df-sup 5976  df-pnf 7097  df-mnf 7098  df-xr 7099  df-ltxr 7100  df-le 7101  df-sub 7226  df-neg 7228  df-div 7452  df-n 7691  df-n0 7861  df-z 7905  df-uz 8025  df-q 8107
Copyright terms: Public domain