![]() |
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 13365 | . . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
2 | 1 | biimpa 476 | . . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
3 | 2 | simp2d 1140 | . 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
4 | 3 | 3impa 1107 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 ∈ wcel 2098 class class class wbr 5138 (class class class)co 7401 ℝ*cxr 11244 ≤ cle 11246 [,]cicc 13324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6485 df-fun 6535 df-fv 6541 df-ov 7404 df-oprab 7405 df-mpo 7406 df-xr 11249 df-icc 13328 |
This theorem is referenced by: xrge0neqmnf 13426 supicc 13475 ttgcontlem1 28611 xrge0infss 32442 xrge0addgt0 32657 xrge0adddir 32658 esumcst 33550 esumpinfval 33560 oms0 33785 probmeasb 33918 broucube 37012 areaquad 42454 lefldiveq 44487 xadd0ge 44515 xrge0nemnfd 44527 eliccelioc 44719 iccintsng 44721 eliccnelico 44727 eliccelicod 44728 ge0xrre 44729 inficc 44732 iccdificc 44737 iccgelbd 44741 cncfiooiccre 45096 iblspltprt 45174 itgioocnicc 45178 itgspltprt 45180 itgiccshift 45181 fourierdlem1 45309 fourierdlem20 45328 fourierdlem24 45332 fourierdlem25 45333 fourierdlem27 45335 fourierdlem43 45351 fourierdlem44 45352 fourierdlem50 45357 fourierdlem51 45358 fourierdlem52 45359 fourierdlem64 45371 fourierdlem73 45380 fourierdlem76 45383 fourierdlem81 45388 fourierdlem92 45399 fourierdlem102 45409 fourierdlem103 45410 fourierdlem104 45411 fourierdlem114 45421 rrxsnicc 45501 salgencntex 45544 fge0iccico 45571 gsumge0cl 45572 sge0sn 45580 sge0tsms 45581 sge0cl 45582 sge0ge0 45585 sge0fsum 45588 sge0pr 45595 sge0prle 45602 sge0p1 45615 sge0rernmpt 45623 meage0 45676 omessre 45711 omeiunltfirp 45720 carageniuncllem2 45723 omege0 45734 ovnlerp 45763 ovn0lem 45766 hoidmvlelem1 45796 hoidmvlelem2 45797 hoidmvlelem3 45798 |
Copyright terms: Public domain | W3C validator |