MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elioore Unicode version

Theorem elioore 10775
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
StepHypRef Expression
1 elioo3g 10774 . 2  |-  ( A  e.  ( B (,) C )  <->  ( ( B  e.  RR*  /\  C  e.  RR*  /\  A  e. 
RR* )  /\  ( B  <  A  /\  A  <  C ) ) )
2 3ancomb 943 . . 3  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  A  e. 
RR* )  <->  ( B  e.  RR*  /\  A  e. 
RR*  /\  C  e.  RR* ) )
3 xrre2 10588 . . 3  |-  ( ( ( B  e.  RR*  /\  A  e.  RR*  /\  C  e.  RR* )  /\  ( B  <  A  /\  A  <  C ) )  ->  A  e.  RR )
42, 3sylanb 458 . 2  |-  ( ( ( B  e.  RR*  /\  C  e.  RR*  /\  A  e.  RR* )  /\  ( B  <  A  /\  A  <  C ) )  ->  A  e.  RR )
51, 4sylbi 187 1  |-  ( A  e.  ( B (,) C )  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    e. wcel 1710   class class class wbr 4102  (class class class)co 5942   RRcr 8823   RR*cxr 8953    < clt 8954   (,)cioo 10745
This theorem is referenced by:  iooval2  10778  elioo4g  10800  ioossre  10801  tgioo  18398  zcld  18415  ioorcl2  19025  lhop2  19460  dvcvx  19465  pilem2  19929  pilem3  19930  pire  19933  tanrpcl  19973  tangtx  19974  tanabsge  19975  sinq34lt0t  19978  cosq14gt0  19979  sineq0  19990  cosne0  19993  tanord  20001  divlogrlim  20087  logno1  20088  logccv  20115  angpieqvd  20233  asinsin  20293  reasinsin  20297  scvxcvx  20385  basellem3  20426  basellem8  20431  vmalogdivsum2  20793  vmalogdivsum  20794  2vmadivsumlem  20795  selberg3lem1  20812  selberg3  20814  selberg4lem1  20815  selberg4  20816  selberg3r  20824  selberg4r  20825  selberg34r  20826  pntrlog2bndlem1  20832  pntrlog2bndlem2  20833  pntrlog2bndlem3  20834  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  pntrlog2bndlem6a  20837  pntrlog2bndlem6  20838  pntpbnd  20843  pntibndlem3  20847  pntibnd  20848  itg2gt0cn  25495  itggt0cn  25512  ftc1cnnclem  25513  ftc1cnnc  25514  dvreasin  25515  dvreacos  25516  areacirclem2  25517  areacirclem3  25518  areacirc  25523  wallispilem1  27137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-cnex 8880  ax-resscn 8881  ax-pre-lttri 8898  ax-pre-lttrn 8899
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-po 4393  df-so 4394  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-1st 6206  df-2nd 6207  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-ioo 10749
  Copyright terms: Public domain W3C validator