![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elicod | Structured version Visualization version GIF version |
Description: Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
elicod.a | ⊢ (𝜑 → 𝐴 ∈ ℝ*) |
elicod.b | ⊢ (𝜑 → 𝐵 ∈ ℝ*) |
elicod.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ*) |
elicod.4 | ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
elicod.5 | ⊢ (𝜑 → 𝐶 < 𝐵) |
Ref | Expression |
---|---|
elicod | ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicod.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℝ*) | |
2 | elicod.4 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐶) | |
3 | elicod.5 | . 2 ⊢ (𝜑 → 𝐶 < 𝐵) | |
4 | elicod.a | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*) | |
5 | elicod.b | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*) | |
6 | elico1 12631 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) | |
7 | 4, 5, 6 | syl2anc 584 | . 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) |
8 | 1, 2, 3, 7 | mpbir3and 1335 | 1 ⊢ (𝜑 → 𝐶 ∈ (𝐴[,)𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ w3a 1080 ∈ wcel 2081 class class class wbr 4962 (class class class)co 7016 ℝ*cxr 10520 < clt 10521 ≤ cle 10522 [,)cico 12590 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-iota 6189 df-fun 6227 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-xr 10525 df-ico 12594 |
This theorem is referenced by: fprodge1 15182 metustexhalf 22849 absfico 41021 icoiccdif 41342 icoopn 41343 eliccnelico 41347 eliccelicod 41348 ge0xrre 41349 uzinico 41378 fsumge0cl 41396 limsupresico 41523 limsuppnfdlem 41524 limsupmnflem 41543 liminfresico 41594 limsup10exlem 41595 liminflelimsupuz 41608 xlimmnfvlem2 41656 icocncflimc 41713 fourierdlem41 41975 fourierdlem46 41979 fourierdlem48 41981 fouriersw 42058 fge0iccico 42194 sge0tsms 42204 sge0repnf 42210 sge0pr 42218 sge0iunmptlemre 42239 sge0rpcpnf 42245 sge0rernmpt 42246 sge0ad2en 42255 sge0xaddlem2 42258 voliunsge0lem 42296 meassre 42301 meaiuninclem 42304 omessre 42334 omeiunltfirp 42343 hoiprodcl 42371 hoicvr 42372 ovnsubaddlem1 42394 hoiprodcl3 42404 hoidmvcl 42406 hoidmv1lelem3 42417 hoidmvlelem3 42421 hoidmvlelem5 42423 hspdifhsp 42440 hoiqssbllem1 42446 hoiqssbllem2 42447 hspmbllem2 42451 volicorege0 42461 ovolval5lem1 42476 iunhoiioolem 42499 preimaicomnf 42532 mod42tp1mod8 43249 eenglngeehlnmlem2 44206 itscnhlinecirc02p 44253 |
Copyright terms: Public domain | W3C validator |