Theorem elioore 13328

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5085  (class class class)co 7367  ℝcr 11037  ℝ^*cxr 11178   < clt 11179  (,)cioo 13298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-ioo 13302

This theorem is referenced by:  iooval2  13331  elioo4g  13359  ioossre  13360  zltaddlt1le  13458  tgioo  24761  zcld  24779  ioorcl2  25539  lhop2  25982  dvcvx  25987  pilem2  26417  pilem3  26418  pire  26421  tanrpcl  26468  tangtx  26469  tanabsge  26470  sinq34lt0t  26473  cosq14gt0  26474  sineq0  26488  cos02pilt1  26490  cosne0  26493  cos0pilt1  26496  tanord  26502  divlogrlim  26599  logno1  26600  logccv  26627  angpieqvd  26795  asinsin  26856  reasinsin  26860  scvxcvx  26949  basellem3  27046  basellem8  27051  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6a  27545  pntrlog2bndlem6  27546  pntpbnd  27551  pntibndlem3  27555  pntibnd  27556  knoppndvlem3  36774  iooelexlt  37678  relowlssretop  37679  relowlpssretop  37680  tan2h  37933  itg2gt0cn  37996  itggt0cn  38011  ftc1cnnclem  38012  ftc1cnnc  38013  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  dvasin  38025  areacirclem1  38029  areacirc  38034  lcmineqlem12  42479  dvrelog2b  42505  0nonelalab  42506  dvrelogpow2b  42507  aks4d1p1p6  42512  aks4d1p1p5  42514  redvmptabs  42792  cvgdvgrat  44740  iooabslt  45929  iocopn  45950  iooshift  45952  icoopn  45955  iooiinicc  45972  elioored  45979  iooiinioc  45986  islptre  46049  limciccioolb  46051  limcicciooub  46065  lptre2pt  46068  xlimxrre  46259  sinaover2ne0  46296  icccncfext  46315  cncfiooicclem1  46321  dvbdfbdioolem2  46357  itgcoscmulx  46397  iblcncfioo  46406  wallispilem1  46493  dirkeritg  46530  dirkercncflem2  46532  fourierdlem27  46562  fourierdlem28  46563  fourierdlem31  46566  fourierdlem32  46567  fourierdlem33  46568  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem47  46581  fourierdlem48  46582  fourierdlem49  46583  fourierdlem56  46590  fourierdlem57  46591  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem64  46598  fourierdlem68  46602  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem81  46615  fourierdlem84  46618  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem100  46634  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  etransclem23  46685  etransclem46  46708  smfaddlem1  47191  amgmwlem  50277