![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elicc2 | Structured version Visualization version GIF version |
Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
Ref | Expression |
---|---|
elicc2 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 11197 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 11197 | . . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | elicc1 13300 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
4 | 1, 2, 3 | syl2an 596 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
5 | mnfxr 11208 | . . . . . . . 8 ⊢ -∞ ∈ ℝ* | |
6 | 5 | a1i 11 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ*) |
7 | 1 | ad2antrr 724 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ*) |
8 | simpr1 1194 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ*) | |
9 | mnflt 13036 | . . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | |
10 | 9 | ad2antrr 724 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐴) |
11 | simpr2 1195 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ≤ 𝐶) | |
12 | 6, 7, 8, 10, 11 | xrltletrd 13072 | . . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶) |
13 | 2 | ad2antlr 725 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ*) |
14 | pnfxr 11205 | . . . . . . . 8 ⊢ +∞ ∈ ℝ* | |
15 | 14 | a1i 11 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ*) |
16 | simpr3 1196 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵) | |
17 | ltpnf 13033 | . . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) | |
18 | 17 | ad2antlr 725 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞) |
19 | 8, 13, 15, 16, 18 | xrlelttrd 13071 | . . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞) |
20 | xrrebnd 13079 | . . . . . . 7 ⊢ (𝐶 ∈ ℝ* → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞))) | |
21 | 8, 20 | syl 17 | . . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ↔ (-∞ < 𝐶 ∧ 𝐶 < +∞))) |
22 | 12, 19, 21 | mpbir2and 711 | . . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ) |
23 | 22, 11, 16 | 3jca 1128 | . . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
24 | 23 | ex 413 | . . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
25 | rexr 11197 | . . . 4 ⊢ (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*) | |
26 | 25 | 3anim1i 1152 | . . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
27 | 24, 26 | impbid1 224 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
28 | 4, 27 | bitrd 278 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 ∈ wcel 2106 class class class wbr 5103 (class class class)co 7353 ℝcr 11046 +∞cpnf 11182 -∞cmnf 11183 ℝ*cxr 11184 < clt 11185 ≤ cle 11186 [,]cicc 13259 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7668 ax-cnex 11103 ax-resscn 11104 ax-pre-lttri 11121 ax-pre-lttrn 11122 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-po 5543 df-so 5544 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-ov 7356 df-oprab 7357 df-mpo 7358 df-er 8644 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11187 df-mnf 11188 df-xr 11189 df-ltxr 11190 df-le 11191 df-icc 13263 |
This theorem is referenced by: elicc2i 13322 iccssre 13338 iccsupr 13351 iccneg 13381 iccsplit 13394 iccshftr 13395 iccshftl 13397 iccdil 13399 icccntr 13401 iccf1o 13405 supicc 13410 icco1 15414 iccntr 24168 icccmplem1 24169 icccmplem2 24170 icccmplem3 24171 reconnlem1 24173 reconnlem2 24174 cnmpopc 24275 icoopnst 24286 iocopnst 24287 cnheiborlem 24301 ivthlem2 24800 ivthlem3 24801 ivthicc 24806 evthicc2 24808 ovolficc 24816 ovolicc1 24864 ovolicc2lem2 24866 ovolicc2lem5 24869 ovolicopnf 24872 dyadmaxlem 24945 opnmbllem 24949 volsup2 24953 volcn 24954 mbfi1fseqlem6 25069 itgspliticc 25185 itgsplitioo 25186 ditgcl 25206 ditgswap 25207 ditgsplitlem 25208 ditgsplit 25209 dvlip 25341 dvlip2 25343 dveq0 25348 dvgt0lem1 25350 dvivthlem1 25356 dvne0 25359 dvcnvrelem1 25365 dvcnvrelem2 25366 dvcnvre 25367 dvfsumlem2 25375 ftc1lem1 25383 ftc1lem2 25384 ftc1a 25385 ftc1lem4 25387 ftc2 25392 ftc2ditglem 25393 itgsubstlem 25396 pserulm 25765 loglesqrt 26095 log2tlbnd 26279 ppisval 26437 chtleppi 26542 fsumvma2 26546 chpchtsum 26551 chpub 26552 rplogsumlem2 26817 chpdifbndlem1 26885 pntibndlem2a 26922 pntibndlem2 26923 pntlemj 26935 pntlem3 26941 pntleml 26943 resconn 33709 cvmliftlem10 33757 opnmbllem0 36081 ftc2nc 36127 areacirclem2 36134 areacirclem4 36136 areacirc 36138 isbnd3 36210 isbnd3b 36211 prdsbnd 36219 iccbnd 36266 intlewftc 40485 dvrelog2 40488 aks4d1p1p5 40499 eliccd 43674 eliccre 43675 iccshift 43688 iccsuble 43689 limcicciooub 43810 icccncfext 44060 itgsubsticc 44149 iblcncfioo 44151 itgiccshift 44153 itgperiod 44154 itgsbtaddcnst 44155 fourierdlem42 44322 fourierdlem54 44333 fourierdlem63 44342 fourierdlem65 44344 fourierdlem74 44353 fourierdlem75 44354 fourierdlem82 44361 fourierdlem93 44372 fourierdlem101 44380 fourierdlem104 44383 fourierdlem111 44390 reorelicc 46728 |
Copyright terms: Public domain | W3C validator |