![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > icogelb | Structured version Visualization version GIF version |
Description: An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
icogelb | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elico1 13299 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵))) | |
2 | simp2 1137 | . . 3 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → 𝐴 ≤ 𝐶) | |
3 | 1, 2 | syl6bi 252 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,)𝐵) → 𝐴 ≤ 𝐶)) |
4 | 3 | 3impia 1117 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 ∈ wcel 2106 class class class wbr 5103 (class class class)co 7353 ℝ*cxr 11184 < clt 11185 ≤ cle 11186 [,)cico 13258 |
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 5254 ax-nul 5261 ax-pr 5382 ax-un 7668 ax-cnex 11103 ax-resscn 11104 |
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 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6445 df-fun 6495 df-fv 6501 df-ov 7356 df-oprab 7357 df-mpo 7358 df-xr 11189 df-ico 13262 |
This theorem is referenced by: fprodge0 15868 fprodge1 15870 hgt750lemf 33135 xralrple2 43524 icoopn 43695 icogelbd 43728 fsumge0cl 43746 limcresioolb 43816 fourierdlem41 44321 fourierdlem43 44323 fourierdlem46 44325 fourierdlem48 44327 fouriersw 44404 sge0isum 44600 sge0ad2en 44604 sge0uzfsumgt 44617 sge0seq 44619 sge0reuz 44620 hoidmv1lelem2 44765 hoidmvlelem1 44768 hoidmvlelem2 44769 ovnhoilem1 44774 hspdifhsp 44789 hspmbllem2 44800 iinhoiicclem 44846 |
Copyright terms: Public domain | W3C validator |