![]() |
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 12614 | . . . 4 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)) | |
2 | elioo2 12598 | . . . 4 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ (𝐵(,)𝐶) ↔ (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶))) |
4 | 3 | ibi 259 | . 2 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
5 | 3simpc 1130 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝐴 ∈ (𝐵(,)𝐶) → (𝐵 < 𝐴 ∧ 𝐴 < 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 ∈ wcel 2050 class class class wbr 4930 (class class class)co 6978 ℝcr 10336 ℝ*cxr 10475 < clt 10476 (,)cioo 12557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-cnex 10393 ax-resscn 10394 ax-pre-lttri 10411 ax-pre-lttrn 10412 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-iun 4795 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-po 5327 df-so 5328 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-ov 6981 df-oprab 6982 df-mpo 6983 df-1st 7503 df-2nd 7504 df-er 8091 df-en 8309 df-dom 8310 df-sdom 8311 df-pnf 10478 df-mnf 10479 df-xr 10480 df-ltxr 10481 df-le 10482 df-ioo 12561 |
This theorem is referenced by: elioo4g 12616 iccssioo2 12628 qdensere 23084 zcld 23127 reconnlem2 23141 xrge0tsms 23148 ovolioo 23875 ioorcl2 23879 itgsplitioo 24144 dvferm1lem 24287 dvferm2lem 24289 dvferm 24291 dvlt0 24308 dvivthlem1 24311 lhop1lem 24316 lhop1 24317 lhop2 24318 dvcvx 24323 ftc1lem4 24342 itgsubstlem 24351 itgsubst 24352 pilem2 24746 pilem3 24747 pigt2lt4 24748 tangtx 24797 tanabsge 24798 cosne0 24818 tanord 24826 tanregt0 24827 argimlt0 24900 logneg2 24902 divlogrlim 24922 logno1 24923 logcnlem3 24931 dvloglem 24935 logf1o2 24937 loglesqrt 25043 asinsin 25174 acoscos 25175 atanlogaddlem 25195 atanlogsub 25198 atantan 25205 atanbndlem 25207 scvxcvx 25268 lgamgulmlem2 25312 basellem8 25370 vmalogdivsum2 25819 vmalogdivsum 25820 2vmadivsumlem 25821 chpdifbndlem1 25834 selberg3lem1 25838 selberg3 25840 selberg4lem1 25841 selberg4 25842 selberg3r 25850 selberg4r 25851 selberg34r 25852 pntrlog2bndlem1 25858 pntrlog2bndlem2 25859 pntrlog2bndlem3 25860 pntrlog2bndlem4 25861 pntrlog2bndlem5 25862 pntrlog2bndlem6a 25863 pntrlog2bndlem6 25864 pntrlog2bnd 25865 pntpbnd1a 25866 pntpbnd1 25867 pntpbnd2 25868 pntpbnd 25869 pntibndlem2 25872 pntibndlem3 25873 pntibnd 25874 pntlemd 25875 pntlemb 25878 pntlemr 25883 pnt 25895 padicabv 25911 xrge0tsmsd 30530 fct2relem 31516 logdivsqrle 31569 knoppndvlem3 33373 iooelexlt 34085 relowlssretop 34086 poimir 34366 itg2gt0cn 34388 ftc1cnnclem 34406 radcnvrat 40062 cncfiooicclem1 41607 itgioocnicc 41693 iblcncfioo 41694 amgmwlem 44271 |
Copyright terms: Public domain | W3C validator |