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 12879 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ w3a 1088 ∈ wcel 2113 class class class wbr 5027 (class class class)co 7164 ℝcr 10607 ≤ cle 10747 [,]cicc 12817 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 ax-pre-lttri 10682 ax-pre-lttrn 10683 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-ov 7167 df-oprab 7168 df-mpo 7169 df-er 8313 df-en 8549 df-dom 8550 df-sdom 8551 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-icc 12821 |
This theorem is referenced by: elicc01 12933 sinbnd2 15620 cosbnd2 15621 iihalf1 23676 iihalf2 23678 elii1 23680 elii2 23681 xrhmeo 23691 oprpiece1res2 23697 pco0 23759 pcoval2 23761 pcoass 23769 vitalilem2 24354 vitali 24358 coseq00topi 25239 coseq0negpitopi 25240 sinq12ge0 25245 cosq14ge0 25248 cosordlem 25266 cosord 25267 cos11 25269 sinord 25270 recosf1o 25271 resinf1o 25272 efif1olem3 25280 argregt0 25345 argrege0 25346 argimgt0 25347 logimul 25349 cxpsqrtlem 25437 acosbnd 25630 log2ub 25679 emcllem7 25731 emgt0 25736 harmonicbnd3 25737 harmoniclbnd 25738 harmonicubnd 25739 harmonicbnd4 25740 logdivbnd 26284 pntpbnd2 26315 sin2h 35379 cos2h 35380 lhe4.4ex1a 41469 fourierdlem40 43214 fourierdlem62 43235 fourierdlem78 43251 fourierdlem111 43284 sqwvfoura 43295 sqwvfourb 43296 |
Copyright terms: Public domain | W3C validator |