![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lbicc2 | Structured version Visualization version Unicode version |
Description: The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.) |
Ref | Expression |
---|---|
lbicc2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 1009 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | xrleid 11439 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 3ad2ant1 1030 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | simp3 1011 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | elicc1 11670 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | 3adant3 1029 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 3, 4, 6 | mpbir3and 1192 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-8 1893 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pow 4554 ax-pr 4612 ax-un 6571 ax-cnex 9582 ax-resscn 9583 ax-pre-lttri 9600 ax-pre-lttrn 9601 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-pw 3921 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-br 4375 df-opab 4434 df-mpt 4435 df-id 4727 df-po 4733 df-so 4734 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-iota 5525 df-fun 5563 df-fn 5564 df-f 5565 df-f1 5566 df-fo 5567 df-f1o 5568 df-fv 5569 df-ov 6279 df-oprab 6280 df-mpt2 6281 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-pnf 9664 df-mnf 9665 df-xr 9666 df-ltxr 9667 df-le 9668 df-icc 11632 |
This theorem is referenced by: icccmplem1 21851 reconnlem2 21856 oprpiece1res1 21990 pcoass 22066 ivthlem1 22413 ivth2 22417 ivthle 22418 ivthle2 22419 evthicc 22421 ovolicc2lem5 22486 dyadmaxlem 22567 rolle 22954 cmvth 22955 mvth 22956 dvlip 22957 c1liplem1 22960 dveq0 22964 dvgt0lem1 22966 lhop1lem 22977 dvcnvrelem1 22981 dvcvx 22984 dvfsumle 22985 dvfsumge 22986 dvfsumabs 22987 dvfsumlem2 22991 ftc2 23008 ftc2ditglem 23009 itgparts 23011 itgsubstlem 23012 taylfval 23326 tayl0 23329 efcvx 23416 pige3 23484 logccv 23620 loglesqrt 23710 eliccioo 28408 oms0OLD 29135 cvmliftlem6 30019 cvmliftlem8 30021 cvmliftlem9 30022 cvmliftlem10 30023 cvmliftlem13 30025 ivthALT 30997 ftc2nc 32028 areacirc 32039 itgpowd 36101 iccintsng 37665 icccncfext 37807 cncfiooicclem1 37813 dvbdfbdioolem1 37842 itgsin0pilem1 37868 itgcoscmulx 37888 itgsincmulx 37893 fourierdlem20 38046 fourierdlem51 38078 fourierdlem54 38081 fourierdlem64 38091 fourierdlem73 38100 fourierdlem81 38108 fourierdlem102 38129 fourierdlem103 38130 fourierdlem104 38131 fourierdlem114 38141 etransclem46 38202 hoidmv1lelem1 38476 |
Copyright terms: Public domain | W3C validator |