![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iccgelb | Structured version Visualization version GIF version |
Description: An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
Ref | Expression |
---|---|
iccgelb | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc1 12508 | . . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
2 | 1 | biimpa 470 | . . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
3 | 2 | simp2d 1179 | . 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
4 | 3 | 3impa 1142 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1113 ∈ wcel 2166 class class class wbr 4874 (class class class)co 6906 ℝ*cxr 10391 ≤ cle 10393 [,]cicc 12467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 ax-un 7210 ax-cnex 10309 ax-resscn 10310 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-iota 6087 df-fun 6126 df-fv 6132 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-xr 10396 df-icc 12471 |
This theorem is referenced by: xrge0neqmnf 12566 supicc 12614 ttgcontlem1 26185 xrge0infss 30073 xrge0addgt0 30237 xrge0adddir 30238 esumcst 30671 esumpinfval 30681 oms0 30905 probmeasb 31039 broucube 33988 areaquad 38645 lefldiveq 40305 xadd0ge 40334 xrge0nemnfd 40346 eliccelioc 40544 iccintsng 40546 eliccnelico 40552 eliccelicod 40553 ge0xrre 40554 inficc 40557 iccdificc 40562 iccgelbd 40566 cncfiooiccre 40904 iblspltprt 40984 itgioocnicc 40988 itgspltprt 40990 itgiccshift 40991 fourierdlem1 41120 fourierdlem20 41139 fourierdlem24 41143 fourierdlem25 41144 fourierdlem27 41146 fourierdlem43 41162 fourierdlem44 41163 fourierdlem50 41168 fourierdlem51 41169 fourierdlem52 41170 fourierdlem64 41182 fourierdlem73 41191 fourierdlem76 41194 fourierdlem81 41199 fourierdlem92 41210 fourierdlem102 41220 fourierdlem103 41221 fourierdlem104 41222 fourierdlem114 41232 rrxsnicc 41312 salgencntex 41353 fge0iccico 41379 gsumge0cl 41380 sge0sn 41388 sge0tsms 41389 sge0cl 41390 sge0ge0 41393 sge0fsum 41396 sge0pr 41403 sge0prle 41410 sge0p1 41423 sge0rernmpt 41431 meage0 41484 omessre 41519 omeiunltfirp 41528 carageniuncllem2 41531 omege0 41542 ovnlerp 41571 ovn0lem 41574 hoidmvlelem1 41604 hoidmvlelem2 41605 hoidmvlelem3 41606 |
Copyright terms: Public domain | W3C validator |