![]() |
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 13382 | . . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | |
2 | elioo2 13365 | . . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) |
4 | 3 | ibi 267 | . 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
5 | 3simpc 1151 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 ∈ wcel 2107 class class class wbr 5149 (class class class)co 7409 ℝcr 11109 ℝ*cxr 11247 < clt 11248 (,)cioo 13324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-1st 7975 df-2nd 7976 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-ioo 13328 |
This theorem is referenced by: elioo4g 13384 iccssioo2 13397 qdensere 24286 zcld 24329 reconnlem2 24343 xrge0tsms 24350 ovolioo 25085 ioorcl2 25089 itgsplitioo 25355 dvferm1lem 25501 dvferm2lem 25503 dvferm 25505 dvlt0 25522 dvivthlem1 25525 lhop1lem 25530 lhop1 25531 lhop2 25532 dvcvx 25537 ftc1lem4 25556 itgsubstlem 25565 itgsubst 25566 pilem2 25964 pilem3 25965 pigt2lt4 25966 tangtx 26015 tanabsge 26016 cosne0 26038 cos0pilt1 26041 tanord 26047 tanregt0 26048 argimlt0 26121 logneg2 26123 divlogrlim 26143 logno1 26144 logcnlem3 26152 dvloglem 26156 logf1o2 26158 loglesqrt 26266 asinsin 26397 acoscos 26398 atanlogaddlem 26418 atanlogsub 26421 atantan 26428 atanbndlem 26430 scvxcvx 26490 lgamgulmlem2 26534 basellem8 26592 vmalogdivsum2 27041 vmalogdivsum 27042 2vmadivsumlem 27043 chpdifbndlem1 27056 selberg3lem1 27060 selberg3 27062 selberg4lem1 27063 selberg4 27064 selberg3r 27072 selberg4r 27073 selberg34r 27074 pntrlog2bndlem1 27080 pntrlog2bndlem2 27081 pntrlog2bndlem3 27082 pntrlog2bndlem4 27083 pntrlog2bndlem5 27084 pntrlog2bndlem6a 27085 pntrlog2bndlem6 27086 pntrlog2bnd 27087 pntpbnd1a 27088 pntpbnd1 27089 pntpbnd2 27090 pntpbnd 27091 pntibndlem2 27094 pntibndlem3 27095 pntibnd 27096 pntlemd 27097 pntlemb 27100 pntlemr 27105 pnt 27117 padicabv 27133 xrge0tsmsd 32209 fct2relem 33609 logdivsqrle 33662 knoppndvlem3 35390 iooelexlt 36243 relowlssretop 36244 poimir 36521 itg2gt0cn 36543 ftc1cnnclem 36559 aks4d1p1p5 40940 radcnvrat 43073 cncfiooicclem1 44609 itgioocnicc 44693 iblcncfioo 44694 amgmwlem 47849 |
Copyright terms: Public domain | W3C validator |