Theorem elioore 13418

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 13417	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) ↔ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ∧ (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
2		3ancomb 1116	. . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) ↔ (𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
3		xrre2 13212	. . 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 2146   class class class wbr 5111  (class class class)co 7419  ℝcr 11114  ℝ^*cxr 11257   < clt 11258  (,)cioo 13388

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-pre-lttri 11189  ax-pre-lttrn 11190

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-ioo 13392

This theorem is used by:  iooval2  13421  elioo4g  13449  ioossre  13450  zltaddlt1le  13548  tgioo  25004  zcld  25022  ioorcl2  25782  lhop2  26225  dvcvx  26230  pilem2  26666  pilem3  26667  pire  26670  tanrpcl  26720  tangtx  26721  tanabsge  26722  sinq34lt0t  26725  cosq14gt0  26726  sineq0  26740  cos02pilt1  26742  cosne0  26745  cos0pilt1  26748  tanord  26754  divlogrlim  26851  logno1  26852  logccv  26879  angpieqvd  27047  asinsin  27108  reasinsin  27112  scvxcvx  27201  basellem3  27298  basellem8  27303  vmalogdivsum2  27753  vmalogdivsum  27754  2vmadivsumlem  27755  selberg3lem1  27772  selberg3  27774  selberg4lem1  27775  selberg4  27776  selberg3r  27784  selberg4r  27785  selberg34r  27786  pntrlog2bndlem1  27792  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntrlog2bndlem6a  27797  pntrlog2bndlem6  27798  pntpbnd  27803  pntibndlem3  27807  pntibnd  27808  knoppndvlem3  37160  iooelexlt  38065  relowlssretop  38066  relowlpssretop  38067  tan2h  38320  itg2gt0cn  38383  itggt0cn  38398  ftc1cnnclem  38399  ftc1cnnc  38400  ftc1anclem7  38407  ftc1anclem8  38408  ftc1anc  38409  dvasin  38412  areacirclem1  38416  areacirc  38421  lcmineqlem12  42865  dvrelog2b  42891  0nonelalab  42892  dvrelogpow2b  42893  aks4d1p1p6  42898  aks4d1p1p5  42900  redvmptabs  43179  cvgdvgrat  45081  iooabslt  46273  iocopn  46294  iooshift  46296  icoopn  46299  iooiinicc  46316  elioored  46323  iooiinioc  46330  islptre  46393  limciccioolb  46395  limcicciooub  46409  lptre2pt  46412  xlimxrre  46603  sinaover2ne0  46640  icccncfext  46659  cncfiooicclem1  46665  dvbdfbdioolem2  46701  itgcoscmulx  46741  iblcncfioo  46750  wallispilem1  46837  dirkeritg  46874  dirkercncflem2  46876  fourierdlem27  46906  fourierdlem28  46907  fourierdlem31  46910  fourierdlem32  46911  fourierdlem33  46912  fourierdlem39  46918  fourierdlem40  46919  fourierdlem41  46920  fourierdlem47  46925  fourierdlem48  46926  fourierdlem49  46927  fourierdlem56  46934  fourierdlem57  46935  fourierdlem59  46937  fourierdlem60  46938  fourierdlem61  46939  fourierdlem62  46940  fourierdlem64  46942  fourierdlem68  46946  fourierdlem72  46950  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem78  46956  fourierdlem81  46959  fourierdlem84  46962  fourierdlem89  46967  fourierdlem90  46968  fourierdlem91  46969  fourierdlem92  46970  fourierdlem93  46971  fourierdlem97  46975  fourierdlem100  46978  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem112  46990  sqwvfoura  47000  sqwvfourb  47001  fouriersw  47003  etransclem23  47029  etransclem46  47052  smfaddlem1  47535  amgmwlem  50707