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 12770 | . . . 4 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
2 | 1 | biimpa 480 | . . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵)) |
3 | 2 | simp2d 1140 | . 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
4 | 3 | 3impa 1107 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 ∈ wcel 2111 class class class wbr 5030 (class class class)co 7135 ℝ*cxr 10663 ≤ cle 10665 [,]cicc 12729 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-xr 10668 df-icc 12733 |
This theorem is referenced by: xrge0neqmnf 12830 supicc 12879 ttgcontlem1 26679 xrge0infss 30510 xrge0addgt0 30725 xrge0adddir 30726 esumcst 31432 esumpinfval 31442 oms0 31665 probmeasb 31798 broucube 35091 areaquad 40166 lefldiveq 41924 xadd0ge 41952 xrge0nemnfd 41964 eliccelioc 42158 iccintsng 42160 eliccnelico 42166 eliccelicod 42167 ge0xrre 42168 inficc 42171 iccdificc 42176 iccgelbd 42180 cncfiooiccre 42537 iblspltprt 42615 itgioocnicc 42619 itgspltprt 42621 itgiccshift 42622 fourierdlem1 42750 fourierdlem20 42769 fourierdlem24 42773 fourierdlem25 42774 fourierdlem27 42776 fourierdlem43 42792 fourierdlem44 42793 fourierdlem50 42798 fourierdlem51 42799 fourierdlem52 42800 fourierdlem64 42812 fourierdlem73 42821 fourierdlem76 42824 fourierdlem81 42829 fourierdlem92 42840 fourierdlem102 42850 fourierdlem103 42851 fourierdlem104 42852 fourierdlem114 42862 rrxsnicc 42942 salgencntex 42983 fge0iccico 43009 gsumge0cl 43010 sge0sn 43018 sge0tsms 43019 sge0cl 43020 sge0ge0 43023 sge0fsum 43026 sge0pr 43033 sge0prle 43040 sge0p1 43053 sge0rernmpt 43061 meage0 43114 omessre 43149 omeiunltfirp 43158 carageniuncllem2 43161 omege0 43172 ovnlerp 43201 ovn0lem 43204 hoidmvlelem1 43234 hoidmvlelem2 43235 hoidmvlelem3 43236 |
Copyright terms: Public domain | W3C validator |