![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elicc1 | Structured version Visualization version GIF version |
Description: Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
elicc1 | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-icc 13271 | . 2 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) | |
2 | 1 | elixx1 13273 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 ∈ wcel 2106 class class class wbr 5105 (class class class)co 7357 ℝ*cxr 11188 ≤ cle 11190 [,]cicc 13267 |
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 5256 ax-nul 5263 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 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 2889 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-sbc 3740 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-xr 11193 df-icc 13271 |
This theorem is referenced by: iccid 13309 iccleub 13319 iccgelb 13320 elicc2 13329 elicc4 13331 elxrge0 13374 lbicc2 13381 ubicc2 13382 difreicc 13401 cnblcld 24138 ovolf 24846 volivth 24971 itg2ge0 25100 itg2const2 25106 taylfvallem1 25716 tayl0 25721 radcnvcl 25776 radcnvle 25779 psercnlem1 25784 eliccelico 31680 xrdifh 31683 unitssxrge0 32481 esumle 32657 esumlef 32661 esumpinfsum 32676 voliune 32828 volfiniune 32829 ddemeas 32835 prob01 33013 elicc3 34789 ftc1cnnclem 36149 ftc1anc 36159 ftc2nc 36160 dvle2 40529 iocinico 41532 icoiccdif 43752 iblsplit 44197 iblspltprt 44204 itgspltprt 44210 fourierdlem1 44339 iccpartrn 45612 rrxsphere 46824 |
Copyright terms: Public domain | W3C validator |