Theorem elioore 13401

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

Step	Hyp	Ref	Expression
1		elioo3g 13400	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1114	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13195	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 592	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2149   class class class wbr 5113  (class class class)co 7411  ℝcr 11098  ℝ^*cxr 11241   < clt 11242  (,)cioo 13371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156  ax-pre-lttri 11173  ax-pre-lttrn 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-ioo 13375

This theorem is referenced by:  iooval2  13404  elioo4g  13432  ioossre  13433  zltaddlt1le  13531  tgioo  24921  zcld  24939  ioorcl2  25699  lhop2  26142  dvcvx  26147  pilem2  26580  pilem3  26581  pire  26584  tanrpcl  26634  tangtx  26635  tanabsge  26636  sinq34lt0t  26639  cosq14gt0  26640  sineq0  26654  cos02pilt1  26656  cosne0  26659  cos0pilt1  26662  tanord  26668  divlogrlim  26765  logno1  26766  logccv  26793  angpieqvd  26961  asinsin  27022  reasinsin  27026  scvxcvx  27115  basellem3  27212  basellem8  27217  vmalogdivsum2  27667  vmalogdivsum  27668  2vmadivsumlem  27669  selberg3lem1  27686  selberg3  27688  selberg4lem1  27689  selberg4  27690  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6a  27711  pntrlog2bndlem6  27712  pntpbnd  27717  pntibndlem3  27721  pntibnd  27722  knoppndvlem3  36991  iooelexlt  37895  relowlssretop  37896  relowlpssretop  37897  tan2h  38150  itg2gt0cn  38213  itggt0cn  38228  ftc1cnnclem  38229  ftc1cnnc  38230  ftc1anclem7  38237  ftc1anclem8  38238  ftc1anc  38239  dvasin  38242  areacirclem1  38246  areacirc  38251  lcmineqlem12  42696  dvrelog2b  42722  0nonelalab  42723  dvrelogpow2b  42724  aks4d1p1p6  42729  aks4d1p1p5  42731  redvmptabs  43010  cvgdvgrat  44914  iooabslt  46106  iocopn  46127  iooshift  46129  icoopn  46132  iooiinicc  46149  elioored  46156  iooiinioc  46163  islptre  46226  limciccioolb  46228  limcicciooub  46242  lptre2pt  46245  xlimxrre  46436  sinaover2ne0  46473  icccncfext  46492  cncfiooicclem1  46498  dvbdfbdioolem2  46534  itgcoscmulx  46574  iblcncfioo  46583  wallispilem1  46670  dirkeritg  46707  dirkercncflem2  46709  fourierdlem27  46739  fourierdlem28  46740  fourierdlem31  46743  fourierdlem32  46744  fourierdlem33  46745  fourierdlem39  46751  fourierdlem40  46752  fourierdlem41  46753  fourierdlem47  46758  fourierdlem48  46759  fourierdlem49  46760  fourierdlem56  46767  fourierdlem57  46768  fourierdlem59  46770  fourierdlem60  46771  fourierdlem61  46772  fourierdlem62  46773  fourierdlem64  46775  fourierdlem68  46779  fourierdlem72  46783  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem78  46789  fourierdlem81  46792  fourierdlem84  46795  fourierdlem89  46800  fourierdlem90  46801  fourierdlem91  46802  fourierdlem92  46803  fourierdlem93  46804  fourierdlem97  46808  fourierdlem100  46811  fourierdlem101  46812  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem112  46823  sqwvfoura  46833  sqwvfourb  46834  fouriersw  46836  etransclem23  46862  etransclem46  46885  smfaddlem1  47368  amgmwlem  50475