![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iccleub | Structured version Visualization version GIF version |
Description: An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
Ref | Expression |
---|---|
iccleub | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc1 12632 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) | |
2 | simp3 1131 | . . 3 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵) → 𝐶 ≤ 𝐵) | |
3 | 1, 2 | syl6bi 254 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐵)) |
4 | 3 | 3impia 1110 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ (𝐴[,]𝐵)) → 𝐶 ≤ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 ∈ wcel 2081 class class class wbr 4962 (class class class)co 7016 ℝ*cxr 10520 ≤ cle 10522 [,]cicc 12591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-iota 6189 df-fun 6227 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-xr 10525 df-icc 12595 |
This theorem is referenced by: supicc 12736 supiccub 12737 supicclub 12738 oprpiece1res1 23238 ivthlem1 23735 isosctrlem1 25077 ttgcontlem1 26354 broucube 34457 mblfinlem1 34460 ftc1cnnclem 34496 ftc2nc 34507 areaquad 39308 isosctrlem1ALT 40807 lefldiveq 41100 eliccelioc 41339 iccintsng 41341 eliccnelico 41347 eliccelicod 41348 inficc 41352 iccdificc 41357 iccleubd 41366 cncfiooiccre 41719 itgioocnicc 41803 itgspltprt 41805 itgiccshift 41806 fourierdlem1 41935 fourierdlem20 41954 fourierdlem24 41958 fourierdlem25 41959 fourierdlem27 41961 fourierdlem43 41977 fourierdlem44 41978 fourierdlem50 41983 fourierdlem51 41984 fourierdlem52 41985 fourierdlem64 41997 fourierdlem73 42006 fourierdlem76 42009 fourierdlem79 42012 fourierdlem81 42014 fourierdlem92 42025 fourierdlem102 42035 fourierdlem103 42036 fourierdlem104 42037 fourierdlem114 42047 rrxsnicc 42127 salgencntex 42168 sge0p1 42238 hoidmv1lelem3 42417 hoidmvlelem1 42419 hoidmvlelem4 42422 |
Copyright terms: Public domain | W3C validator |