![]() |
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 11159 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 11159 | . . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | elicc1 13262 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
4 | 1, 2, 3 | syl2an 596 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
5 | mnfxr 11170 | . . . . . . . 8 ⊢ -∞ ∈ ℝ* | |
6 | 5 | a1i 11 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ ∈ ℝ*) |
7 | 1 | ad2antrr 724 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ∈ ℝ*) |
8 | simpr1 1194 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ∈ ℝ*) | |
9 | mnflt 12998 | . . . . . . . 8 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) | |
10 | 9 | ad2antrr 724 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐴) |
11 | simpr2 1195 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐴 ≤ 𝐶) | |
12 | 6, 7, 8, 10, 11 | xrltletrd 13034 | . . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → -∞ < 𝐶) |
13 | 2 | ad2antlr 725 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 ∈ ℝ*) |
14 | pnfxr 11167 | . . . . . . . 8 ⊢ +∞ ∈ ℝ* | |
15 | 14 | a1i 11 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → +∞ ∈ ℝ*) |
16 | simpr3 1196 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 ≤ 𝐵) | |
17 | ltpnf 12995 | . . . . . . . 8 ⊢ (𝐵 ∈ ℝ → 𝐵 < +∞) | |
18 | 17 | ad2antlr 725 | . . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐵 < +∞) |
19 | 8, 13, 15, 16, 18 | xrlelttrd 13033 | . . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) → 𝐶 < +∞) |
20 | xrrebnd 13041 | . . . . . . 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 11159 | . . . 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 7351 ℝcr 11008 +∞cpnf 11144 -∞cmnf 11145 ℝ*cxr 11146 < clt 11147 ≤ cle 11148 [,]cicc 13221 |
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 2708 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7664 ax-cnex 11065 ax-resscn 11066 ax-pre-lttri 11083 ax-pre-lttrn 11084 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 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 7354 df-oprab 7355 df-mpo 7356 df-er 8606 df-en 8842 df-dom 8843 df-sdom 8844 df-pnf 11149 df-mnf 11150 df-xr 11151 df-ltxr 11152 df-le 11153 df-icc 13225 |
This theorem is referenced by: elicc2i 13284 iccssre 13300 iccsupr 13313 iccneg 13343 iccsplit 13356 iccshftr 13357 iccshftl 13359 iccdil 13361 icccntr 13363 iccf1o 13367 supicc 13372 icco1 15382 iccntr 24136 icccmplem1 24137 icccmplem2 24138 icccmplem3 24139 reconnlem1 24141 reconnlem2 24142 cnmpopc 24243 icoopnst 24254 iocopnst 24255 cnheiborlem 24269 ivthlem2 24768 ivthlem3 24769 ivthicc 24774 evthicc2 24776 ovolficc 24784 ovolicc1 24832 ovolicc2lem2 24834 ovolicc2lem5 24837 ovolicopnf 24840 dyadmaxlem 24913 opnmbllem 24917 volsup2 24921 volcn 24922 mbfi1fseqlem6 25037 itgspliticc 25153 itgsplitioo 25154 ditgcl 25174 ditgswap 25175 ditgsplitlem 25176 ditgsplit 25177 dvlip 25309 dvlip2 25311 dveq0 25316 dvgt0lem1 25318 dvivthlem1 25324 dvne0 25327 dvcnvrelem1 25333 dvcnvrelem2 25334 dvcnvre 25335 dvfsumlem2 25343 ftc1lem1 25351 ftc1lem2 25352 ftc1a 25353 ftc1lem4 25355 ftc2 25360 ftc2ditglem 25361 itgsubstlem 25364 pserulm 25733 loglesqrt 26063 log2tlbnd 26247 ppisval 26405 chtleppi 26510 fsumvma2 26514 chpchtsum 26519 chpub 26520 rplogsumlem2 26785 chpdifbndlem1 26853 pntibndlem2a 26890 pntibndlem2 26891 pntlemj 26903 pntlem3 26909 pntleml 26911 resconn 33652 cvmliftlem10 33700 opnmbllem0 36052 ftc2nc 36098 areacirclem2 36105 areacirclem4 36107 areacirc 36109 isbnd3 36181 isbnd3b 36182 prdsbnd 36190 iccbnd 36237 intlewftc 40456 dvrelog2 40459 aks4d1p1p5 40470 eliccd 43643 eliccre 43644 iccshift 43657 iccsuble 43658 limcicciooub 43779 icccncfext 44029 itgsubsticc 44118 iblcncfioo 44120 itgiccshift 44122 itgperiod 44123 itgsbtaddcnst 44124 fourierdlem42 44291 fourierdlem54 44302 fourierdlem63 44311 fourierdlem65 44313 fourierdlem74 44322 fourierdlem75 44323 fourierdlem82 44330 fourierdlem93 44341 fourierdlem101 44349 fourierdlem104 44352 fourierdlem111 44359 reorelicc 46697 |
Copyright terms: Public domain | W3C validator |