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 13394

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 13386	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 ∈ ℝ^ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵)))
2		simp2 1149	. . 3 ⊢ ((𝐶 ∈ ℝ^* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵) → 𝐴 ≤ 𝐶)
3	1, 2	biimtrdi 255	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴[,)𝐵) → 𝐴 ≤ 𝐶))
4	3	3impia 1129	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1097 ∈ wcel 2141 class class class wbr 5097 (class class class)co 7391 ℝ^*cxr 11209 < clt 11210 ≤ cle 11211 [,)cico 13345

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-sbc 3743 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-id 5538 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-iota 6472 df-fun 6518 df-fv 6524 df-ov 7394 df-oprab 7395 df-mpo 7396 df-xr 11214 df-ico 13349

This theorem is referenced by: icogelbd 13395 fprodge0 16014 fprodge1 16016 hgt750lemf 34908 xralrple2 45891 icoopn 46062 fsumge0cl 46110 limcresioolb 46178 fourierdlem41 46683 fourierdlem43 46685 fourierdlem46 46687 fouriersw 46766 sge0isum 46962 sge0ad2en 46966 sge0uzfsumgt 46979 sge0seq 46981 sge0reuz 46982 hoidmv1lelem2 47127 hoidmvlelem1 47130 hoidmvlelem2 47131 ovnhoilem1 47136 hspdifhsp 47151 hspmbllem2 47162 iinhoiicclem 47208

W3C validator