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 13449

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 ∈ wcel 2145 class class class wbr 5103 (class class class)co 7413 ℝ^*cxr 11266 < clt 11267 ≤ cle 11268 [,)cico 13400

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5251 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3740 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-iota 6489 df-fun 6535 df-fv 6541 df-ov 7416 df-oprab 7417 df-mpo 7418 df-xr 11271 df-ico 13404

This theorem is used by: icogelbd 13450 fprodge0 16080 fprodge1 16082 hgt750lemf 35161 xralrple2 46184 icoopn 46355 fsumge0cl 46403 limcresioolb 46471 fourierdlem41 46976 fourierdlem43 46978 fourierdlem46 46980 fouriersw 47059 sge0isum 47255 sge0ad2en 47259 sge0uzfsumgt 47272 sge0seq 47274 sge0reuz 47275 hoidmv1lelem2 47420 hoidmvlelem1 47423 hoidmvlelem2 47424 ovnhoilem1 47429 hspdifhsp 47444 hspmbllem2 47455 iinhoiicclem 47501

W3C validator