![]() |
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 1134 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ*) | |
2 | xrleid 13154 | . . 3 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴) | |
3 | 2 | 3ad2ant1 1131 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐴) |
4 | simp3 1136 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) | |
5 | elicc1 13392 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) | |
6 | 5 | 3adant3 1130 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ (𝐴[,]𝐵) ↔ (𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
7 | 1, 3, 4, 6 | mpbir3and 1340 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1085 ∈ wcel 2099 class class class wbr 5142 (class class class)co 7414 ℝ*cxr 11269 ≤ cle 11271 [,]cicc 13351 |
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 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-pre-lttri 11204 ax-pre-lttrn 11205 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-opab 5205 df-mpt 5226 df-id 5570 df-po 5584 df-so 5585 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7417 df-oprab 7418 df-mpo 7419 df-er 8718 df-en 8956 df-dom 8957 df-sdom 8958 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-icc 13355 |
This theorem is referenced by: icccmplem1 24725 reconnlem2 24730 oprpiece1res1 24863 pcoass 24938 ivthlem1 25367 ivth2 25371 ivthle 25372 ivthle2 25373 evthicc 25375 ovolicc2lem5 25437 dyadmaxlem 25513 rolle 25909 cmvth 25910 cmvthOLD 25911 mvth 25912 dvlip 25913 c1liplem1 25916 dveq0 25920 dvgt0lem1 25922 lhop1lem 25933 dvcnvrelem1 25937 dvcvx 25940 dvfsumle 25941 dvfsumleOLD 25942 dvfsumge 25943 dvfsumabs 25944 dvfsumlem2 25948 dvfsumlem2OLD 25949 ftc2 25966 ftc2ditglem 25967 itgparts 25969 itgsubstlem 25970 itgpowd 25972 taylfval 26280 tayl0 26283 efcvx 26373 pige3ALT 26441 logccv 26584 loglesqrt 26680 eliccioo 32636 ftc2re 34166 cvmliftlem6 34836 cvmliftlem8 34838 cvmliftlem9 34839 cvmliftlem10 34840 cvmliftlem13 34842 ivthALT 35755 ftc2nc 37110 areacirc 37121 iccintsng 44831 icccncfext 45198 cncfiooicclem1 45204 dvbdfbdioolem1 45239 itgsin0pilem1 45261 itgcoscmulx 45280 itgsincmulx 45285 fourierdlem20 45438 fourierdlem51 45468 fourierdlem54 45471 fourierdlem64 45481 fourierdlem73 45490 fourierdlem81 45498 fourierdlem102 45519 fourierdlem103 45520 fourierdlem104 45521 fourierdlem114 45531 etransclem46 45591 hoidmv1lelem1 45902 |
Copyright terms: Public domain | W3C validator |