![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iccleub | Structured version Visualization version Unicode 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 11708 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp3 1016 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6bi 236 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 3impia 1212 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 ax-un 6609 ax-cnex 9620 ax-resscn 9621 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-sbc 3279 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-opab 4475 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-iota 5564 df-fun 5602 df-fv 5608 df-ov 6317 df-oprab 6318 df-mpt2 6319 df-xr 9704 df-icc 11670 |
This theorem is referenced by: supicc 11808 supiccub 11809 supicclub 11810 oprpiece1res1 22027 ivthlem1 22450 isosctrlem1 23795 ttgcontlem1 24963 broucube 32018 mblfinlem1 32021 ftc1cnnclem 32059 ftc2nc 32070 areaquad 36145 isosctrlem1ALT 37370 lefldiveq 37543 eliccelioc 37659 iccintsng 37661 eliccnelico 37668 eliccelicod 37669 inficc 37673 iccdificc 37678 cncfiooiccre 37810 itgioocnicc 37891 itgspltprt 37893 itgiccshift 37894 fourierdlem1 38007 fourierdlem20 38026 fourierdlem24 38030 fourierdlem25 38031 fourierdlem27 38033 fourierdlem43 38051 fourierdlem44 38052 fourierdlem50 38057 fourierdlem51 38058 fourierdlem52 38059 fourierdlem64 38071 fourierdlem73 38080 fourierdlem76 38083 fourierdlem79 38086 fourierdlem81 38088 fourierdlem92 38099 fourierdlem102 38109 fourierdlem103 38110 fourierdlem104 38111 fourierdlem114 38121 salgencntex 38239 sge0p1 38293 hoidmv1lelem3 38452 hoidmvlelem1 38454 hoidmvlelem4 38457 |
Copyright terms: Public domain | W3C validator |