Theorem elioore 11695

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	|- ( A e. ( B (,) C ) -> A e. RR )

Proof of Theorem elioore

Step	Hyp	Ref	Expression
1		elioo3g 11694	. 2 |- ( A e. ( B (,) C ) <-> ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) /\ ( B < A /\ A < C ) ) )
2		3ancomb 1000	. . 3 |- ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) <-> ( B e. RR* /\ A e. RR* /\ C e. RR* ) )
3		xrre2 11494	. . 3 |- ( ( ( B e. RR* /\ A e. RR* /\ C e. RR* ) /\ ( B < A /\ A < C ) ) -> A e. RR )
4	2, 3	sylanb 479	. 2 |- ( ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) /\ ( B < A /\ A < C ) ) -> A e. RR )
5	1, 4	sylbi 200	1 |- ( A e. ( B (,) C ) -> A e. RR )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991   e. wcel 1898   class class class wbr 4416  (class class class)co 6315   RRcr 9564   RR*cxr 9700   < clt 9701   (,)cioo 11664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-pre-lttri 9639  ax-pre-lttrn 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-ioo 11668

This theorem is referenced by:  iooval2  11698  elioo4g  11724  ioossre  11725  tgioo  21863  zcld  21880  ioorcl2  22573  lhop2  23016  dvcvx  23021  pilem2  23456  pilem2OLD  23457  pilem3  23458  pilem3OLD  23459  pire  23462  tanrpcl  23508  tangtx  23509  tanabsge  23510  sinq34lt0t  23513  cosq14gt0  23514  sineq0  23525  cosne0  23528  tanord  23536  divlogrlim  23629  logno1  23630  logccv  23657  angpieqvd  23806  asinsin  23867  reasinsin  23871  scvxcvx  23960  basellem3  24058  basellem8  24063  vmalogdivsum2  24425  vmalogdivsum  24426  2vmadivsumlem  24427  selberg3lem1  24444  selberg3  24446  selberg4lem1  24447  selberg4  24448  selberg3r  24456  selberg4r  24457  selberg34r  24458  pntrlog2bndlem1  24464  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntrlog2bndlem6a  24469  pntrlog2bndlem6  24470  pntpbnd  24475  pntibndlem3  24479  pntibnd  24480  iooelexlt  31810  relowlssretop  31811  relowlpssretop  31812  tan2h  31982  dvtanlemOLD  32036  itg2gt0cn  32042  itggt0cn  32059  ftc1cnnclem  32060  ftc1cnnc  32061  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  dvasin  32073  areacirclem1  32077  areacirc  32082  cvgdvgrat  36706  iooabslt  37634  iocopn  37659  iooshift  37661  icoopn  37664  islptre  37737  limciccioolb  37739  limcicciooub  37755  lptre2pt  37758  limcresiooub  37761  limcresioolb  37762  sinaover2ne0  37781  icccncfext  37803  cncfiooicclem1  37809  dvbdfbdioolem2  37839  itgcoscmulx  37884  iblcncfioo  37893  wallispilem1  37965  dirkeritg  38002  dirkercncflem1  38003  dirkercncflem2  38004  fourierdlem27  38034  fourierdlem28  38035  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem32  38040  fourierdlem33  38041  fourierdlem39  38047  fourierdlem40  38048  fourierdlem41  38049  fourierdlem47  38055  fourierdlem48  38056  fourierdlem49  38057  fourierdlem56  38064  fourierdlem57  38065  fourierdlem59  38067  fourierdlem60  38068  fourierdlem61  38069  fourierdlem62  38070  fourierdlem64  38072  fourierdlem68  38076  fourierdlem72  38080  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem81  38089  fourierdlem84  38092  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem92  38100  fourierdlem93  38101  fourierdlem97  38105  fourierdlem100  38108  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fourierdlem112  38120  sqwvfoura  38130  sqwvfourb  38131  fouriersw  38133  etransclem23  38160  etransclem46  38183