icogelb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > icogelb		Structured version Visualization version GIF version

Theorem icogelb 13340

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.)

**Assertion**
Ref	Expression
icogelb	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶)

**Proof of Theorem icogelb**
Step	Hyp	Ref	Expression
1		elico1 13332	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
2		simp2 1138	. . 3 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → 𝐴 ≤ 𝐶)
3	1, 2	biimtrdi 253	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) → 𝐴 ≤ 𝐶))
4	3	3impia 1118	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ∈ wcel 2114 class class class wbr 5086 (class class class)co 7360 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 [,)cico 13291

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-xr 11174 df-ico 13295

This theorem is referenced by: icogelbd 13341 fprodge0 15949 fprodge1 15951 hgt750lemf 34813 xralrple2 45802 icoopn 45973 fsumge0cl 46021 limcresioolb 46089 fourierdlem41 46594 fourierdlem43 46596 fourierdlem46 46598 fourierdlem48 46600 fouriersw 46677 sge0isum 46873 sge0ad2en 46877 sge0uzfsumgt 46890 sge0seq 46892 sge0reuz 46893 hoidmv1lelem2 47038 hoidmvlelem1 47041 hoidmvlelem2 47042 ovnhoilem1 47047 hspdifhsp 47062 hspmbllem2 47073 iinhoiicclem 47119

W3C validator