Theorem elioore 13428

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 13427	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1116	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13222	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 593	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7413  ℝcr 11123  ℝ^*cxr 11266   < clt 11267  (,)cioo 13398

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-pre-lttri 11198  ax-pre-lttrn 11199

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-ioo 13402

This theorem is used by:  iooval2  13431  elioo4g  13459  ioossre  13460  zltaddlt1le  13558  tgioo  25022  zcld  25040  ioorcl2  25800  lhop2  26242  dvcvx  26247  pilem2  26688  pilem3  26689  pire  26692  tanrpcl  26742  tangtx  26743  tanabsge  26744  sinq34lt0t  26747  cosq14gt0  26748  sineq0  26761  cos02pilt1  26763  cosne0  26766  cos0pilt1  26769  tanord  26775  divlogrlim  26872  logno1  26873  logccv  26900  angpieqvd  27068  asinsin  27129  reasinsin  27133  scvxcvx  27222  basellem3  27319  basellem8  27324  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  selberg3lem1  27793  selberg3  27795  selberg4lem1  27796  selberg4  27797  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6a  27818  pntrlog2bndlem6  27819  pntpbnd  27824  pntibndlem3  27828  pntibnd  27829  knoppndvlem3  37211  iooelexlt  38116  relowlssretop  38117  relowlpssretop  38118  tan2h  38366  itg2gt0cn  38424  itggt0cn  38439  ftc1cnnclem  38440  ftc1cnnc  38441  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  dvasin  38453  areacirclem1  38457  areacirc  38462  lcmineqlem12  42906  dvrelog2b  42932  0nonelalab  42933  dvrelogpow2b  42934  aks4d1p1p6  42939  aks4d1p1p5  42941  redvmptabs  43235  cvgdvgrat  45137  iooabslt  46329  iocopn  46350  iooshift  46352  icoopn  46355  iooiinicc  46372  elioored  46379  iooiinioc  46386  islptre  46449  limciccioolb  46451  limcicciooub  46465  lptre2pt  46468  xlimxrre  46659  sinaover2ne0  46696  icccncfext  46715  cncfiooicclem1  46721  dvbdfbdioolem2  46757  itgcoscmulx  46797  iblcncfioo  46806  wallispilem1  46893  dirkeritg  46930  dirkercncflem2  46932  fourierdlem27  46962  fourierdlem28  46963  fourierdlem31  46966  fourierdlem32  46967  fourierdlem33  46968  fourierdlem39  46974  fourierdlem40  46975  fourierdlem41  46976  fourierdlem47  46981  fourierdlem48  46982  fourierdlem49  46983  fourierdlem56  46990  fourierdlem57  46991  fourierdlem59  46993  fourierdlem60  46994  fourierdlem61  46995  fourierdlem62  46996  fourierdlem64  46998  fourierdlem68  47002  fourierdlem72  47006  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem81  47015  fourierdlem84  47018  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem93  47027  fourierdlem97  47031  fourierdlem100  47034  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem23  47085  etransclem46  47108  smfaddlem1  47591  amgmwlem  50820