Theorem elioore 13365

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 13364	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1107	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13159	. . 3 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
4	2, 3	sylanb 589	. 2 ⊢ (((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) → 𝐴 ∈ ℝ)
5	1, 4	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095   ∈ wcel 2132   class class class wbr 5090  (class class class)co 7381  ℝcr 11058  ℝ^*cxr 11201   < clt 11202  (,)cioo 13335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-1st 7955  df-2nd 7956  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208  df-ioo 13339

This theorem is referenced by:  iooval2  13368  elioo4g  13396  ioossre  13397  zltaddlt1le  13495  tgioo  24825  zcld  24843  ioorcl2  25603  lhop2  26046  dvcvx  26051  pilem2  26481  pilem3  26482  pire  26485  tanrpcl  26535  tangtx  26536  tanabsge  26537  sinq34lt0t  26540  cosq14gt0  26541  sineq0  26555  cos02pilt1  26557  cosne0  26560  cos0pilt1  26563  tanord  26569  divlogrlim  26666  logno1  26667  logccv  26694  angpieqvd  26862  asinsin  26923  reasinsin  26927  scvxcvx  27016  basellem3  27113  basellem8  27118  vmalogdivsum2  27568  vmalogdivsum  27569  2vmadivsumlem  27570  selberg3lem1  27587  selberg3  27589  selberg4lem1  27590  selberg4  27591  selberg3r  27599  selberg4r  27600  selberg34r  27601  pntrlog2bndlem1  27607  pntrlog2bndlem2  27608  pntrlog2bndlem3  27609  pntrlog2bndlem4  27610  pntrlog2bndlem5  27611  pntrlog2bndlem6a  27612  pntrlog2bndlem6  27613  pntpbnd  27618  pntibndlem3  27622  pntibnd  27623  knoppndvlem3  36890  iooelexlt  37794  relowlssretop  37795  relowlpssretop  37796  tan2h  38049  itg2gt0cn  38112  itggt0cn  38127  ftc1cnnclem  38128  ftc1cnnc  38129  ftc1anclem7  38136  ftc1anclem8  38137  ftc1anc  38138  dvasin  38141  areacirclem1  38145  areacirc  38150  lcmineqlem12  42595  dvrelog2b  42621  0nonelalab  42622  dvrelogpow2b  42623  aks4d1p1p6  42628  aks4d1p1p5  42630  redvmptabs  42907  cvgdvgrat  44827  iooabslt  46013  iocopn  46034  iooshift  46036  icoopn  46039  iooiinicc  46056  elioored  46063  iooiinioc  46070  islptre  46133  limciccioolb  46135  limcicciooub  46149  lptre2pt  46152  xlimxrre  46343  sinaover2ne0  46380  icccncfext  46399  cncfiooicclem1  46405  dvbdfbdioolem2  46441  itgcoscmulx  46481  iblcncfioo  46490  wallispilem1  46577  dirkeritg  46614  dirkercncflem2  46616  fourierdlem27  46646  fourierdlem28  46647  fourierdlem31  46650  fourierdlem32  46651  fourierdlem33  46652  fourierdlem39  46658  fourierdlem40  46659  fourierdlem41  46660  fourierdlem47  46665  fourierdlem48  46666  fourierdlem49  46667  fourierdlem56  46674  fourierdlem57  46675  fourierdlem59  46677  fourierdlem60  46678  fourierdlem61  46679  fourierdlem62  46680  fourierdlem64  46682  fourierdlem68  46686  fourierdlem72  46690  fourierdlem73  46691  fourierdlem74  46692  fourierdlem75  46693  fourierdlem76  46694  fourierdlem78  46696  fourierdlem81  46699  fourierdlem84  46702  fourierdlem89  46707  fourierdlem90  46708  fourierdlem91  46709  fourierdlem92  46710  fourierdlem93  46711  fourierdlem97  46715  fourierdlem100  46718  fourierdlem101  46719  fourierdlem103  46721  fourierdlem104  46722  fourierdlem111  46729  fourierdlem112  46730  sqwvfoura  46740  sqwvfourb  46741  fouriersw  46743  etransclem23  46769  etransclem46  46792  smfaddlem1  47275  amgmwlem  50361