Theorem elioore 13389

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 13388	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1096	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13184	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 579	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   ∈ wcel 2098   class class class wbr 5149  (class class class)co 7419  ℝcr 11139  ℝ^*cxr 11279   < clt 11280  (,)cioo 13359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-pre-lttri 11214  ax-pre-lttrn 11215

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7994  df-2nd 7995  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-ioo 13363

This theorem is referenced by:  iooval2  13392  elioo4g  13419  ioossre  13420  zltaddlt1le  13517  tgioo  24756  zcld  24773  ioorcl2  25545  lhop2  25992  dvcvx  25997  pilem2  26434  pilem3  26435  pire  26438  tanrpcl  26484  tangtx  26485  tanabsge  26486  sinq34lt0t  26489  cosq14gt0  26490  sineq0  26503  cos02pilt1  26505  cosne0  26508  cos0pilt1  26511  tanord  26517  divlogrlim  26614  logno1  26615  logccv  26642  angpieqvd  26808  asinsin  26869  reasinsin  26873  scvxcvx  26963  basellem3  27060  basellem8  27065  vmalogdivsum2  27516  vmalogdivsum  27517  2vmadivsumlem  27518  selberg3lem1  27535  selberg3  27537  selberg4lem1  27538  selberg4  27539  selberg3r  27547  selberg4r  27548  selberg34r  27549  pntrlog2bndlem1  27555  pntrlog2bndlem2  27556  pntrlog2bndlem3  27557  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  pntrlog2bndlem6a  27560  pntrlog2bndlem6  27561  pntpbnd  27566  pntibndlem3  27570  pntibnd  27571  knoppndvlem3  36120  iooelexlt  36972  relowlssretop  36973  relowlpssretop  36974  tan2h  37216  itg2gt0cn  37279  itggt0cn  37294  ftc1cnnclem  37295  ftc1cnnc  37296  ftc1anclem7  37303  ftc1anclem8  37304  ftc1anc  37305  dvasin  37308  areacirclem1  37312  areacirc  37317  lcmineqlem12  41643  dvrelog2b  41669  0nonelalab  41670  dvrelogpow2b  41671  aks4d1p1p6  41676  aks4d1p1p5  41678  cvgdvgrat  43892  iooabslt  45022  iocopn  45043  iooshift  45045  icoopn  45048  iooiinicc  45065  elioored  45072  iooiinioc  45079  islptre  45145  limciccioolb  45147  limcicciooub  45163  lptre2pt  45166  xlimxrre  45357  sinaover2ne0  45394  icccncfext  45413  cncfiooicclem1  45419  dvbdfbdioolem2  45455  itgcoscmulx  45495  iblcncfioo  45504  wallispilem1  45591  dirkeritg  45628  dirkercncflem2  45630  fourierdlem27  45660  fourierdlem28  45661  fourierdlem31  45664  fourierdlem32  45665  fourierdlem33  45666  fourierdlem39  45672  fourierdlem40  45673  fourierdlem41  45674  fourierdlem47  45679  fourierdlem48  45680  fourierdlem49  45681  fourierdlem56  45688  fourierdlem57  45689  fourierdlem59  45691  fourierdlem60  45692  fourierdlem61  45693  fourierdlem62  45694  fourierdlem64  45696  fourierdlem68  45700  fourierdlem72  45704  fourierdlem73  45705  fourierdlem74  45706  fourierdlem75  45707  fourierdlem76  45708  fourierdlem78  45710  fourierdlem81  45713  fourierdlem84  45716  fourierdlem89  45721  fourierdlem90  45722  fourierdlem91  45723  fourierdlem92  45724  fourierdlem93  45725  fourierdlem97  45729  fourierdlem100  45732  fourierdlem101  45733  fourierdlem103  45735  fourierdlem104  45736  fourierdlem111  45743  fourierdlem112  45744  sqwvfoura  45754  sqwvfourb  45755  fouriersw  45757  etransclem23  45783  etransclem46  45806  smfaddlem1  46289  amgmwlem  48421