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 13333

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5102 (class class class)co 7369 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 [,)cico 13284

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-sbc 3751 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-opab 5165 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-iota 6452 df-fun 6501 df-fv 6507 df-ov 7372 df-oprab 7373 df-mpo 7374 df-xr 11188 df-ico 13288

This theorem is referenced by: icogelbd 13334 fprodge0 15935 fprodge1 15937 hgt750lemf 34617 xralrple2 45323 icoopn 45496 fsumge0cl 45544 limcresioolb 45614 fourierdlem41 46119 fourierdlem43 46121 fourierdlem46 46123 fourierdlem48 46125 fouriersw 46202 sge0isum 46398 sge0ad2en 46402 sge0uzfsumgt 46415 sge0seq 46417 sge0reuz 46418 hoidmv1lelem2 46563 hoidmvlelem1 46566 hoidmvlelem2 46567 ovnhoilem1 46572 hspdifhsp 46587 hspmbllem2 46598 iinhoiicclem 46644

W3C validator