Theorem elioore 11617

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 11616	. 2 |- ( A e. ( B (,) C ) <-> ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) /\ ( B < A /\ A < C ) ) )
2		3ancomb 991	. . 3 |- ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) <-> ( B e. RR* /\ A e. RR* /\ C e. RR* ) )
3		xrre2 11416	. . 3 |- ( ( ( B e. RR* /\ A e. RR* /\ C e. RR* ) /\ ( B < A /\ A < C ) ) -> A e. RR )
4	2, 3	sylanb 474	. 2 |- ( ( ( B e. RR* /\ C e. RR* /\ A e. RR* ) /\ ( B < A /\ A < C ) ) -> A e. RR )
5	1, 4	sylbi 198	1 |- ( A e. ( B (,) C ) -> A e. RR )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   e. wcel 1872   class class class wbr 4366  (class class class)co 6249   RRcr 9489   RR*cxr 9625   < clt 9626   (,)cioo 11586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-pre-lttri 9564  ax-pre-lttrn 9565

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-po 4717  df-so 4718  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-1st 6751  df-2nd 6752  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-ioo 11590

This theorem is referenced by:  iooval2  11620  elioo4g  11646  ioossre  11647  tgioo  21756  zcld  21773  ioorcl2  22466  lhop2  22909  dvcvx  22914  pilem2  23349  pilem2OLD  23350  pilem3  23351  pilem3OLD  23352  pire  23355  tanrpcl  23401  tangtx  23402  tanabsge  23403  sinq34lt0t  23406  cosq14gt0  23407  sineq0  23418  cosne0  23421  tanord  23429  divlogrlim  23522  logno1  23523  logccv  23550  angpieqvd  23699  asinsin  23760  reasinsin  23764  scvxcvx  23853  basellem3  23951  basellem8  23956  vmalogdivsum2  24318  vmalogdivsum  24319  2vmadivsumlem  24320  selberg3lem1  24337  selberg3  24339  selberg4lem1  24340  selberg4  24341  selberg3r  24349  selberg4r  24350  selberg34r  24351  pntrlog2bndlem1  24357  pntrlog2bndlem2  24358  pntrlog2bndlem3  24359  pntrlog2bndlem4  24360  pntrlog2bndlem5  24361  pntrlog2bndlem6a  24362  pntrlog2bndlem6  24363  pntpbnd  24368  pntibndlem3  24372  pntibnd  24373  iooelexlt  31672  relowlssretop  31673  relowlpssretop  31674  tan2h  31844  dvtanlemOLD  31898  itg2gt0cn  31904  itggt0cn  31921  ftc1cnnclem  31922  ftc1cnnc  31923  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  dvasin  31935  areacirclem1  31939  areacirc  31944  cvgdvgrat  36575  iooabslt  37488  iocopn  37513  iooshift  37515  icoopn  37518  islptre  37582  limciccioolb  37584  limcicciooub  37600  lptre2pt  37603  limcresiooub  37606  limcresioolb  37607  sinaover2ne0  37626  icccncfext  37648  cncfiooicclem1  37654  dvbdfbdioolem2  37684  itgcoscmulx  37729  iblcncfioo  37738  wallispilem1  37810  dirkeritg  37847  dirkercncflem1  37848  dirkercncflem2  37849  fourierdlem27  37879  fourierdlem28  37880  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem32  37885  fourierdlem33  37886  fourierdlem39  37892  fourierdlem40  37893  fourierdlem41  37894  fourierdlem47  37900  fourierdlem48  37901  fourierdlem49  37902  fourierdlem56  37909  fourierdlem57  37910  fourierdlem59  37912  fourierdlem60  37913  fourierdlem61  37914  fourierdlem62  37915  fourierdlem64  37917  fourierdlem68  37921  fourierdlem72  37925  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem78  37931  fourierdlem81  37934  fourierdlem84  37937  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem92  37945  fourierdlem93  37946  fourierdlem97  37950  fourierdlem100  37953  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem112  37965  sqwvfoura  37975  sqwvfourb  37976  fouriersw  37978  etransclem23  38005  etransclem46  38028