![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eliooord | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
eliooord | ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliooxr 13378 | . . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | |
2 | elioo2 13361 | . . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) |
4 | 3 | ibi 266 | . 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
5 | 3simpc 1150 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 ∈ wcel 2106 class class class wbr 5147 (class class class)co 7405 ℝcr 11105 ℝ*cxr 11243 < clt 11244 (,)cioo 13320 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-pre-lttri 11180 ax-pre-lttrn 11181 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7971 df-2nd 7972 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-ioo 13324 |
This theorem is referenced by: elioo4g 13380 iccssioo2 13393 qdensere 24277 zcld 24320 reconnlem2 24334 xrge0tsms 24341 ovolioo 25076 ioorcl2 25080 itgsplitioo 25346 dvferm1lem 25492 dvferm2lem 25494 dvferm 25496 dvlt0 25513 dvivthlem1 25516 lhop1lem 25521 lhop1 25522 lhop2 25523 dvcvx 25528 ftc1lem4 25547 itgsubstlem 25556 itgsubst 25557 pilem2 25955 pilem3 25956 pigt2lt4 25957 tangtx 26006 tanabsge 26007 cosne0 26029 cos0pilt1 26032 tanord 26038 tanregt0 26039 argimlt0 26112 logneg2 26114 divlogrlim 26134 logno1 26135 logcnlem3 26143 dvloglem 26147 logf1o2 26149 loglesqrt 26255 asinsin 26386 acoscos 26387 atanlogaddlem 26407 atanlogsub 26410 atantan 26417 atanbndlem 26419 scvxcvx 26479 lgamgulmlem2 26523 basellem8 26581 vmalogdivsum2 27030 vmalogdivsum 27031 2vmadivsumlem 27032 chpdifbndlem1 27045 selberg3lem1 27049 selberg3 27051 selberg4lem1 27052 selberg4 27053 selberg3r 27061 selberg4r 27062 selberg34r 27063 pntrlog2bndlem1 27069 pntrlog2bndlem2 27070 pntrlog2bndlem3 27071 pntrlog2bndlem4 27072 pntrlog2bndlem5 27073 pntrlog2bndlem6a 27074 pntrlog2bndlem6 27075 pntrlog2bnd 27076 pntpbnd1a 27077 pntpbnd1 27078 pntpbnd2 27079 pntpbnd 27080 pntibndlem2 27083 pntibndlem3 27084 pntibnd 27085 pntlemd 27086 pntlemb 27089 pntlemr 27094 pnt 27106 padicabv 27122 xrge0tsmsd 32196 fct2relem 33597 logdivsqrle 33650 knoppndvlem3 35378 iooelexlt 36231 relowlssretop 36232 poimir 36509 itg2gt0cn 36531 ftc1cnnclem 36547 aks4d1p1p5 40928 radcnvrat 43058 cncfiooicclem1 44595 itgioocnicc 44679 iblcncfioo 44680 amgmwlem 47802 |
Copyright terms: Public domain | W3C validator |