Theorem eliooord 13353

Description: Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)

Assertion

Ref	Expression
eliooord	⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))

Proof of Theorem eliooord

Step	Hyp	Ref	Expression
1		eliooxr 13352	. . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*))
2		elioo2 13334	. . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
3	1, 2	syl 17	. . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)))
4	3	ibi 267	. 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
5		3simpc 1151	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))
6	4, 5	syl 17	1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7362  ℝcr 11032  ℝ^*cxr 11173   < clt 11174  (,)cioo 13293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107  ax-pre-lttrn 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-po 5534  df-so 5535  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7937  df-2nd 7938  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-ioo 13297

This theorem is referenced by:  elioo4g  13354  iccssioo2  13367  qdensere  24748  zcld  24793  reconnlem2  24807  xrge0tsms  24814  ovolioo  25549  ioorcl2  25553  itgsplitioo  25819  dvferm1lem  25965  dvferm2lem  25967  dvferm  25969  dvlt0  25986  dvivthlem1  25989  lhop1lem  25994  lhop1  25995  lhop2  25996  dvcvx  26001  ftc1lem4  26020  itgsubstlem  26029  itgsubst  26030  pilem2  26434  pilem3  26435  pigt2lt4  26436  tangtx  26486  tanabsge  26487  cosne0  26510  cos0pilt1  26513  tanord  26519  tanregt0  26520  argimlt0  26594  logneg2  26596  divlogrlim  26616  logno1  26617  logcnlem3  26625  dvloglem  26629  logf1o2  26631  loglesqrt  26742  asinsin  26873  acoscos  26874  atanlogaddlem  26894  atanlogsub  26897  atantan  26904  atanbndlem  26906  scvxcvx  26967  lgamgulmlem2  27011  basellem8  27069  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  chpdifbndlem1  27534  selberg3lem1  27538  selberg3  27540  selberg4lem1  27541  selberg4  27542  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6a  27563  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntpbnd  27569  pntibndlem2  27572  pntibndlem3  27573  pntibnd  27574  pntlemd  27575  pntlemb  27578  pntlemr  27583  pnt  27595  padicabv  27611  xrge0tsmsd  33153  fct2relem  34761  logdivsqrle  34814  knoppndvlem3  36794  iooelexlt  37698  relowlssretop  37699  poimir  37994  itg2gt0cn  38016  ftc1cnnclem  38032  aks4d1p1p5  42534  radcnvrat  44765  cncfiooicclem1  46345  itgioocnicc  46429  iblcncfioo  46430  amgmwlem  50295