![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elicc2i | Structured version Visualization version GIF version |
Description: Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
Ref | Expression |
---|---|
elicc2i.1 | ⊢ 𝐴 ∈ ℝ |
elicc2i.2 | ⊢ 𝐵 ∈ ℝ |
Ref | Expression |
---|---|
elicc2i | ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc2i.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
2 | elicc2i.2 | . 2 ⊢ 𝐵 ∈ ℝ | |
3 | elicc2 12429 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
4 | 1, 2, 3 | mp2an 710 | 1 ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ w3a 1072 ∈ wcel 2137 class class class wbr 4802 (class class class)co 6811 ℝcr 10125 ≤ cle 10265 [,]cicc 12369 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-cnex 10182 ax-resscn 10183 ax-pre-lttri 10200 ax-pre-lttrn 10201 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-nel 3034 df-ral 3053 df-rex 3054 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-op 4326 df-uni 4587 df-br 4803 df-opab 4863 df-mpt 4880 df-id 5172 df-po 5185 df-so 5186 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-f1 6052 df-fo 6053 df-f1o 6054 df-fv 6055 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-er 7909 df-en 8120 df-dom 8121 df-sdom 8122 df-pnf 10266 df-mnf 10267 df-xr 10268 df-ltxr 10269 df-le 10270 df-icc 12373 |
This theorem is referenced by: 0elunit 12481 1elunit 12482 divelunit 12505 lincmb01cmp 12506 iccf1o 12507 sinbnd2 15109 cosbnd2 15110 rpnnen2lem12 15151 blcvx 22800 iirev 22927 iihalf1 22929 iihalf2 22931 elii1 22933 elii2 22934 iimulcl 22935 iccpnfhmeo 22943 xrhmeo 22944 oprpiece1res2 22950 lebnumii 22964 htpycc 22978 pco0 23012 pcoval2 23014 pcocn 23015 pcohtpylem 23017 pcopt 23020 pcopt2 23021 pcoass 23022 pcorevlem 23024 vitalilem2 23575 vitali 23579 abelth2 24393 coseq00topi 24451 coseq0negpitopi 24452 sinq12ge0 24457 cosq14ge0 24460 cosordlem 24474 cosord 24475 cos11 24476 sinord 24477 recosf1o 24478 resinf1o 24479 efif1olem3 24487 argregt0 24553 argrege0 24554 argimgt0 24555 logimul 24557 cxpsqrtlem 24645 chordthmlem4 24759 acosbnd 24824 leibpi 24866 log2ub 24873 jensenlem2 24911 emcllem7 24925 emgt0 24930 harmonicbnd3 24931 harmoniclbnd 24932 harmonicubnd 24933 harmonicbnd4 24934 lgamgulmlem2 24953 logdivbnd 25442 pntpbnd2 25473 ttgcontlem1 25962 brbtwn2 25982 ax5seglem1 26005 ax5seglem2 26006 ax5seglem3 26008 ax5seglem5 26010 ax5seglem6 26011 ax5seglem9 26014 ax5seg 26015 axbtwnid 26016 axpaschlem 26017 axpasch 26018 axcontlem2 26042 axcontlem4 26044 axcontlem7 26047 stge0 29390 stle1 29391 strlem3a 29418 elunitrn 30250 elunitge0 30252 unitdivcld 30254 xrge0iifiso 30288 xrge0iifhom 30290 resconn 31533 snmlff 31616 sin2h 33710 cos2h 33711 poimirlem29 33749 poimirlem30 33750 poimirlem31 33751 poimirlem32 33752 lhe4.4ex1a 39028 fourierdlem40 40865 fourierdlem62 40886 fourierdlem78 40902 fourierdlem111 40935 sqwvfoura 40946 sqwvfourb 40947 |
Copyright terms: Public domain | W3C validator |