MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elioore Structured version   Visualization version   GIF version

Theorem elioore 13295
Description: A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
Assertion
Ref Expression
elioore (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Proof of Theorem elioore
StepHypRef Expression
1 elioo3g 13294 . 2 (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)))
2 3ancomb 1100 . . 3 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ℝ*))
3 xrre2 13090 . . 3 (((𝐵 ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
42, 3sylanb 582 . 2 (((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
51, 4sylbi 216 1 (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088  wcel 2107   class class class wbr 5106  (class class class)co 7358  cr 11051  *cxr 11189   < clt 11190  (,)cioo 13265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-pre-lttri 11126  ax-pre-lttrn 11127
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-ioo 13269
This theorem is referenced by:  iooval2  13298  elioo4g  13325  ioossre  13326  zltaddlt1le  13423  tgioo  24162  zcld  24179  ioorcl2  24939  lhop2  25382  dvcvx  25387  pilem2  25814  pilem3  25815  pire  25818  tanrpcl  25864  tangtx  25865  tanabsge  25866  sinq34lt0t  25869  cosq14gt0  25870  sineq0  25883  cos02pilt1  25885  cosne0  25888  cos0pilt1  25891  tanord  25897  divlogrlim  25993  logno1  25994  logccv  26021  angpieqvd  26184  asinsin  26245  reasinsin  26249  scvxcvx  26338  basellem3  26435  basellem8  26440  vmalogdivsum2  26889  vmalogdivsum  26890  2vmadivsumlem  26891  selberg3lem1  26908  selberg3  26910  selberg4lem1  26911  selberg4  26912  selberg3r  26920  selberg4r  26921  selberg34r  26922  pntrlog2bndlem1  26928  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntrlog2bndlem6a  26933  pntrlog2bndlem6  26934  pntpbnd  26939  pntibndlem3  26943  pntibnd  26944  knoppndvlem3  34980  iooelexlt  35836  relowlssretop  35837  relowlpssretop  35838  tan2h  36073  itg2gt0cn  36136  itggt0cn  36151  ftc1cnnclem  36152  ftc1cnnc  36153  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  dvasin  36165  areacirclem1  36169  areacirc  36174  lcmineqlem12  40500  dvrelog2b  40526  0nonelalab  40527  dvrelogpow2b  40528  aks4d1p1p6  40533  aks4d1p1p5  40535  cvgdvgrat  42600  iooabslt  43744  iocopn  43765  iooshift  43767  icoopn  43770  iooiinicc  43787  elioored  43794  iooiinioc  43801  islptre  43867  limciccioolb  43869  limcicciooub  43885  lptre2pt  43888  xlimxrre  44079  sinaover2ne0  44116  icccncfext  44135  cncfiooicclem1  44141  dvbdfbdioolem2  44177  itgcoscmulx  44217  iblcncfioo  44226  wallispilem1  44313  dirkeritg  44350  dirkercncflem2  44352  fourierdlem27  44382  fourierdlem28  44383  fourierdlem31  44386  fourierdlem32  44387  fourierdlem33  44388  fourierdlem39  44394  fourierdlem40  44395  fourierdlem41  44396  fourierdlem47  44401  fourierdlem48  44402  fourierdlem49  44403  fourierdlem56  44410  fourierdlem57  44411  fourierdlem59  44413  fourierdlem60  44414  fourierdlem61  44415  fourierdlem62  44416  fourierdlem64  44418  fourierdlem68  44422  fourierdlem72  44426  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem76  44430  fourierdlem78  44432  fourierdlem81  44435  fourierdlem84  44438  fourierdlem89  44443  fourierdlem90  44444  fourierdlem91  44445  fourierdlem92  44446  fourierdlem93  44447  fourierdlem97  44451  fourierdlem100  44454  fourierdlem101  44455  fourierdlem103  44457  fourierdlem104  44458  fourierdlem111  44465  fourierdlem112  44466  sqwvfoura  44476  sqwvfourb  44477  fouriersw  44479  etransclem23  44505  etransclem46  44528  smfaddlem1  45011  amgmwlem  47256
  Copyright terms: Public domain W3C validator