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 13520

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 13512	. . 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 7418 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 [,)cico 13471

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 2733 ax-sep 5249 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 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 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-iota 6493 df-fun 6539 df-fv 6545 df-ov 7421 df-oprab 7422 df-mpo 7423 df-xr 11340 df-ico 13475

This theorem is used by: icogelbd 13521 fprodge0 16153 fprodge1 16155 hgt750lemf 35275 xralrple2 46335 icoopn 46506 fsumge0cl 46554 limcresioolb 46622 fourierdlem41 47127 fourierdlem43 47129 fourierdlem46 47131 fouriersw 47210 sge0isum 47406 sge0ad2en 47410 sge0uzfsumgt 47423 sge0seq 47425 sge0reuz 47426 hoidmv1lelem2 47571 hoidmvlelem1 47574 hoidmvlelem2 47575 ovnhoilem1 47580 hspdifhsp 47595 hspmbllem2 47606 iinhoiicclem 47652

W3C validator