![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > iooltub | Structured version Visualization version GIF version |
Description: An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
iooltub | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elioo2 12633 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | |
2 | simp3 1131 | . . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵) | |
3 | 1, 2 | syl6bi 254 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) → 𝐶 < 𝐵)) |
4 | 3 | 3impia 1110 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴(,)𝐵)) → 𝐶 < 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 ∈ wcel 2083 class class class wbr 4968 (class class class)co 7023 ℝcr 10389 ℝ*cxr 10527 < clt 10528 (,)cioo 12592 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-resscn 10447 ax-pre-lttri 10464 ax-pre-lttrn 10465 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-1st 7552 df-2nd 7553 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 df-ioo 12596 |
This theorem is referenced by: iooshift 41361 icoopn 41364 iooiinicc 41381 iooltubd 41383 iooiinioc 41395 lptre2pt 41484 limcresiooub 41486 limcresioolb 41487 sinaover2ne0 41712 dvbdfbdioolem1 41776 dvbdfbdioolem2 41777 ioodvbdlimc1lem1 41779 ioodvbdlimc2lem 41782 fourierdlem27 41983 fourierdlem28 41984 fourierdlem40 41996 fourierdlem41 41997 fourierdlem46 42001 fourierdlem48 42003 fourierdlem49 42004 fourierdlem57 42012 fourierdlem59 42014 fourierdlem60 42015 fourierdlem61 42016 fourierdlem62 42017 fourierdlem64 42019 fourierdlem68 42023 fourierdlem73 42028 fourierdlem76 42031 fourierdlem78 42033 fourierdlem84 42039 fourierdlem90 42045 fourierdlem92 42047 fourierdlem97 42052 fourierdlem103 42058 fourierdlem104 42059 fourierdlem111 42066 sqwvfoura 42077 sqwvfourb 42078 fouriersw 42080 etransclem23 42106 qndenserrnbllem 42143 ioorrnopnlem 42153 ioorrnopnxrlem 42155 hspdifhsp 42462 hoiqssbllem1 42468 hoiqssbllem2 42469 hspmbllem2 42473 iunhoiioolem 42521 pimiooltgt 42553 pimdecfgtioo 42559 pimincfltioo 42560 smfaddlem1 42603 smfmullem1 42630 smfmullem2 42631 |
Copyright terms: Public domain | W3C validator |