Theorem elioore 13270

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2111   class class class wbr 5086  (class class class)co 7341  ℝcr 11000  ℝ^*cxr 11140   < clt 11141  (,)cioo 13240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-pre-lttri 11075  ax-pre-lttrn 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-po 5519  df-so 5520  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7916  df-2nd 7917  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-ioo 13244

This theorem is referenced by:  iooval2  13273  elioo4g  13301  ioossre  13302  zltaddlt1le  13400  tgioo  24706  zcld  24724  ioorcl2  25495  lhop2  25942  dvcvx  25947  pilem2  26384  pilem3  26385  pire  26388  tanrpcl  26435  tangtx  26436  tanabsge  26437  sinq34lt0t  26440  cosq14gt0  26441  sineq0  26455  cos02pilt1  26457  cosne0  26460  cos0pilt1  26463  tanord  26469  divlogrlim  26566  logno1  26567  logccv  26594  angpieqvd  26763  asinsin  26824  reasinsin  26828  scvxcvx  26918  basellem3  27015  basellem8  27020  vmalogdivsum2  27471  vmalogdivsum  27472  2vmadivsumlem  27473  selberg3lem1  27490  selberg3  27492  selberg4lem1  27493  selberg4  27494  selberg3r  27502  selberg4r  27503  selberg34r  27504  pntrlog2bndlem1  27510  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  pntrlog2bndlem6a  27515  pntrlog2bndlem6  27516  pntpbnd  27521  pntibndlem3  27525  pntibnd  27526  knoppndvlem3  36548  iooelexlt  37396  relowlssretop  37397  relowlpssretop  37398  tan2h  37652  itg2gt0cn  37715  itggt0cn  37730  ftc1cnnclem  37731  ftc1cnnc  37732  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  dvasin  37744  areacirclem1  37748  areacirc  37753  lcmineqlem12  42073  dvrelog2b  42099  0nonelalab  42100  dvrelogpow2b  42101  aks4d1p1p6  42106  aks4d1p1p5  42108  redvmptabs  42393  cvgdvgrat  44346  iooabslt  45539  iocopn  45560  iooshift  45562  icoopn  45565  iooiinicc  45582  elioored  45589  iooiinioc  45596  islptre  45659  limciccioolb  45661  limcicciooub  45675  lptre2pt  45678  xlimxrre  45869  sinaover2ne0  45906  icccncfext  45925  cncfiooicclem1  45931  dvbdfbdioolem2  45967  itgcoscmulx  46007  iblcncfioo  46016  wallispilem1  46103  dirkeritg  46140  dirkercncflem2  46142  fourierdlem27  46172  fourierdlem28  46173  fourierdlem31  46176  fourierdlem32  46177  fourierdlem33  46178  fourierdlem39  46184  fourierdlem40  46185  fourierdlem41  46186  fourierdlem47  46191  fourierdlem48  46192  fourierdlem49  46193  fourierdlem56  46200  fourierdlem57  46201  fourierdlem59  46203  fourierdlem60  46204  fourierdlem61  46205  fourierdlem62  46206  fourierdlem64  46208  fourierdlem68  46212  fourierdlem72  46216  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem78  46222  fourierdlem81  46225  fourierdlem84  46228  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem92  46236  fourierdlem93  46237  fourierdlem97  46241  fourierdlem100  46244  fourierdlem101  46245  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  fourierdlem112  46256  sqwvfoura  46266  sqwvfourb  46267  fouriersw  46269  etransclem23  46295  etransclem46  46318  smfaddlem1  46801  amgmwlem  49834