Theorem elioore 13282

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2113   class class class wbr 5095  (class class class)co 7355  ℝcr 11016  ℝ^*cxr 11156   < clt 11157  (,)cioo 13252

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-pre-lttri 11091  ax-pre-lttrn 11092

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-1st 7930  df-2nd 7931  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-ioo 13256

This theorem is referenced by:  iooval2  13285  elioo4g  13313  ioossre  13314  zltaddlt1le  13412  tgioo  24731  zcld  24749  ioorcl2  25520  lhop2  25967  dvcvx  25972  pilem2  26409  pilem3  26410  pire  26413  tanrpcl  26460  tangtx  26461  tanabsge  26462  sinq34lt0t  26465  cosq14gt0  26466  sineq0  26480  cos02pilt1  26482  cosne0  26485  cos0pilt1  26488  tanord  26494  divlogrlim  26591  logno1  26592  logccv  26619  angpieqvd  26788  asinsin  26849  reasinsin  26853  scvxcvx  26943  basellem3  27040  basellem8  27045  vmalogdivsum2  27496  vmalogdivsum  27497  2vmadivsumlem  27498  selberg3lem1  27515  selberg3  27517  selberg4lem1  27518  selberg4  27519  selberg3r  27527  selberg4r  27528  selberg34r  27529  pntrlog2bndlem1  27535  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  pntrlog2bndlem6a  27540  pntrlog2bndlem6  27541  pntpbnd  27546  pntibndlem3  27550  pntibnd  27551  knoppndvlem3  36630  iooelexlt  37479  relowlssretop  37480  relowlpssretop  37481  tan2h  37725  itg2gt0cn  37788  itggt0cn  37803  ftc1cnnclem  37804  ftc1cnnc  37805  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  dvasin  37817  areacirclem1  37821  areacirc  37826  lcmineqlem12  42206  dvrelog2b  42232  0nonelalab  42233  dvrelogpow2b  42234  aks4d1p1p6  42239  aks4d1p1p5  42241  redvmptabs  42530  cvgdvgrat  44470  iooabslt  45661  iocopn  45682  iooshift  45684  icoopn  45687  iooiinicc  45704  elioored  45711  iooiinioc  45718  islptre  45781  limciccioolb  45783  limcicciooub  45797  lptre2pt  45800  xlimxrre  45991  sinaover2ne0  46028  icccncfext  46047  cncfiooicclem1  46053  dvbdfbdioolem2  46089  itgcoscmulx  46129  iblcncfioo  46138  wallispilem1  46225  dirkeritg  46262  dirkercncflem2  46264  fourierdlem27  46294  fourierdlem28  46295  fourierdlem31  46298  fourierdlem32  46299  fourierdlem33  46300  fourierdlem39  46306  fourierdlem40  46307  fourierdlem41  46308  fourierdlem47  46313  fourierdlem48  46314  fourierdlem49  46315  fourierdlem56  46322  fourierdlem57  46323  fourierdlem59  46325  fourierdlem60  46326  fourierdlem61  46327  fourierdlem62  46328  fourierdlem64  46330  fourierdlem68  46334  fourierdlem72  46338  fourierdlem73  46339  fourierdlem74  46340  fourierdlem75  46341  fourierdlem76  46342  fourierdlem78  46344  fourierdlem81  46347  fourierdlem84  46350  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem92  46358  fourierdlem93  46359  fourierdlem97  46363  fourierdlem100  46366  fourierdlem101  46367  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  fourierdlem112  46378  sqwvfoura  46388  sqwvfourb  46389  fouriersw  46391  etransclem23  46417  etransclem46  46440  smfaddlem1  46923  amgmwlem  49963