![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lbicc2 | Structured version Visualization version GIF version |
Description: The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.) |
Ref | Expression |
---|---|
lbicc2 | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1133 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ*) | |
2 | xrleid 13186 | . . 3 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) | |
3 | 2 | 3ad2ant1 1130 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐴) |
4 | simp3 1135 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) | |
5 | elicc1 13424 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) | |
6 | 5 | 3adant3 1129 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
7 | 1, 3, 4, 6 | mpbir3and 1339 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1084 ∈ wcel 2099 class class class wbr 5155 (class class class)co 7426 ℝ*cxr 11299 ≤ cle 11301 [,]cicc 13383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5306 ax-nul 5313 ax-pow 5371 ax-pr 5435 ax-un 7748 ax-cnex 11216 ax-resscn 11217 ax-pre-lttri 11234 ax-pre-lttrn 11235 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4916 df-br 5156 df-opab 5218 df-mpt 5239 df-id 5582 df-po 5596 df-so 5597 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-f1 6561 df-fo 6562 df-f1o 6563 df-fv 6564 df-ov 7429 df-oprab 7430 df-mpo 7431 df-er 8736 df-en 8977 df-dom 8978 df-sdom 8979 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-icc 13387 |
This theorem is referenced by: icccmplem1 24832 reconnlem2 24837 oprpiece1res1 24970 pcoass 25045 ivthlem1 25474 ivth2 25478 ivthle 25479 ivthle2 25480 evthicc 25482 ovolicc2lem5 25544 dyadmaxlem 25620 rolle 26016 cmvth 26017 cmvthOLD 26018 mvth 26019 dvlip 26020 c1liplem1 26023 dveq0 26027 dvgt0lem1 26029 lhop1lem 26040 dvcnvrelem1 26044 dvcvx 26047 dvfsumle 26048 dvfsumleOLD 26049 dvfsumge 26050 dvfsumabs 26051 dvfsumlem2 26055 dvfsumlem2OLD 26056 ftc2 26073 ftc2ditglem 26074 itgparts 26076 itgsubstlem 26077 itgpowd 26079 taylfval 26389 tayl0 26392 efcvx 26482 pige3ALT 26550 logccv 26693 loglesqrt 26792 eliccioo 32794 ftc2re 34446 cvmliftlem6 35120 cvmliftlem8 35122 cvmliftlem9 35123 cvmliftlem10 35124 cvmliftlem13 35126 ivthALT 36049 ftc2nc 37405 areacirc 37416 iccintsng 45159 icccncfext 45526 cncfiooicclem1 45532 dvbdfbdioolem1 45567 itgsin0pilem1 45589 itgcoscmulx 45608 itgsincmulx 45613 fourierdlem20 45766 fourierdlem51 45796 fourierdlem54 45799 fourierdlem64 45809 fourierdlem73 45818 fourierdlem81 45826 fourierdlem102 45847 fourierdlem103 45848 fourierdlem104 45849 fourierdlem114 45859 etransclem46 45919 hoidmv1lelem1 46230 |
Copyright terms: Public domain | W3C validator |