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

Theorem elioore 12243
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 12242 . 2 (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)))
2 3ancomb 1064 . . 3 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ℝ*))
3 xrre2 12039 . . 3 (((𝐵 ∈ ℝ*𝐴 ∈ ℝ*𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
42, 3sylanb 488 . 2 (((𝐵 ∈ ℝ*𝐶 ∈ ℝ*𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
51, 4sylbi 207 1 (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054  wcel 2030   class class class wbr 4685  (class class class)co 6690  cr 9973  *cxr 10111   < clt 10112  (,)cioo 12213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-pre-lttri 10048  ax-pre-lttrn 10049
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-ioo 12217
This theorem is referenced by:  iooval2  12246  elioo4g  12272  ioossre  12273  zltaddlt1le  12362  tgioo  22646  zcld  22663  ioorcl2  23386  lhop2  23823  dvcvx  23828  pilem2  24251  pilem3  24252  pire  24255  tanrpcl  24301  tangtx  24302  tanabsge  24303  sinq34lt0t  24306  cosq14gt0  24307  sineq0  24318  cosne0  24321  tanord  24329  divlogrlim  24426  logno1  24427  logccv  24454  angpieqvd  24603  asinsin  24664  reasinsin  24668  scvxcvx  24757  basellem3  24854  basellem8  24859  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  selberg3lem1  25291  selberg3  25293  selberg4lem1  25294  selberg4  25295  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6a  25316  pntrlog2bndlem6  25317  pntpbnd  25322  pntibndlem3  25326  pntibnd  25327  knoppndvlem3  32630  iooelexlt  33340  relowlssretop  33341  relowlpssretop  33342  tan2h  33531  itg2gt0cn  33595  itggt0cn  33612  ftc1cnnclem  33613  ftc1cnnc  33614  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  dvasin  33626  areacirclem1  33630  areacirc  33635  cvgdvgrat  38829  iooabslt  40039  iocopn  40064  iooshift  40066  icoopn  40069  iooiinicc  40087  elioored  40094  iooiinioc  40101  islptre  40169  limciccioolb  40171  limcicciooub  40187  lptre2pt  40190  xlimxrre  40375  sinaover2ne0  40397  icccncfext  40418  cncfiooicclem1  40424  dvbdfbdioolem2  40462  itgcoscmulx  40503  iblcncfioo  40512  wallispilem1  40600  dirkeritg  40637  dirkercncflem2  40639  fourierdlem27  40669  fourierdlem28  40670  fourierdlem31  40673  fourierdlem32  40674  fourierdlem33  40675  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem56  40697  fourierdlem57  40698  fourierdlem59  40700  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem64  40705  fourierdlem68  40709  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem81  40722  fourierdlem84  40725  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem100  40741  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  etransclem23  40792  etransclem46  40815  smfaddlem1  41292  amgmwlem  42876
  Copyright terms: Public domain W3C validator