Theorem elioore 13397

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 13396	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1098	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13191	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 581	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5124  (class class class)co 7410  ℝcr 11133  ℝ^*cxr 11273   < clt 11274  (,)cioo 13367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-pre-lttri 11208  ax-pre-lttrn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7993  df-2nd 7994  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-ioo 13371

This theorem is referenced by:  iooval2  13400  elioo4g  13428  ioossre  13429  zltaddlt1le  13527  tgioo  24740  zcld  24758  ioorcl2  25530  lhop2  25977  dvcvx  25982  pilem2  26419  pilem3  26420  pire  26423  tanrpcl  26470  tangtx  26471  tanabsge  26472  sinq34lt0t  26475  cosq14gt0  26476  sineq0  26490  cos02pilt1  26492  cosne0  26495  cos0pilt1  26498  tanord  26504  divlogrlim  26601  logno1  26602  logccv  26629  angpieqvd  26798  asinsin  26859  reasinsin  26863  scvxcvx  26953  basellem3  27050  basellem8  27055  vmalogdivsum2  27506  vmalogdivsum  27507  2vmadivsumlem  27508  selberg3lem1  27525  selberg3  27527  selberg4lem1  27528  selberg4  27529  selberg3r  27537  selberg4r  27538  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntrlog2bndlem6a  27550  pntrlog2bndlem6  27551  pntpbnd  27556  pntibndlem3  27560  pntibnd  27561  knoppndvlem3  36537  iooelexlt  37385  relowlssretop  37386  relowlpssretop  37387  tan2h  37641  itg2gt0cn  37704  itggt0cn  37719  ftc1cnnclem  37720  ftc1cnnc  37721  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  dvasin  37733  areacirclem1  37737  areacirc  37742  lcmineqlem12  42058  dvrelog2b  42084  0nonelalab  42085  dvrelogpow2b  42086  aks4d1p1p6  42091  aks4d1p1p5  42093  redvmptabs  42378  cvgdvgrat  44312  iooabslt  45508  iocopn  45529  iooshift  45531  icoopn  45534  iooiinicc  45551  elioored  45558  iooiinioc  45565  islptre  45628  limciccioolb  45630  limcicciooub  45646  lptre2pt  45649  xlimxrre  45840  sinaover2ne0  45877  icccncfext  45896  cncfiooicclem1  45902  dvbdfbdioolem2  45938  itgcoscmulx  45978  iblcncfioo  45987  wallispilem1  46074  dirkeritg  46111  dirkercncflem2  46113  fourierdlem27  46143  fourierdlem28  46144  fourierdlem31  46147  fourierdlem32  46148  fourierdlem33  46149  fourierdlem39  46155  fourierdlem40  46156  fourierdlem41  46157  fourierdlem47  46162  fourierdlem48  46163  fourierdlem49  46164  fourierdlem56  46171  fourierdlem57  46172  fourierdlem59  46174  fourierdlem60  46175  fourierdlem61  46176  fourierdlem62  46177  fourierdlem64  46179  fourierdlem68  46183  fourierdlem72  46187  fourierdlem73  46188  fourierdlem74  46189  fourierdlem75  46190  fourierdlem76  46191  fourierdlem78  46193  fourierdlem81  46196  fourierdlem84  46199  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem92  46207  fourierdlem93  46208  fourierdlem97  46212  fourierdlem100  46215  fourierdlem101  46216  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  fourierdlem112  46227  sqwvfoura  46237  sqwvfourb  46238  fouriersw  46240  etransclem23  46266  etransclem46  46289  smfaddlem1  46772  amgmwlem  49646