![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elicc1 | Structured version Visualization version Unicode version |
Description: Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
elicc1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-icc 11670 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | elixx1 11672 |
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: iccid 11709 iccleub 11718 iccgelb 11719 elicc2 11727 elicc4 11729 xrge0neqmnf 11765 elxrge0 11769 lbicc2 11776 ubicc2 11777 difreicc 11792 cnblcld 21843 oprpiece1res1 22027 ovolf 22483 volivth 22613 itg2ge0 22741 itg2const2 22747 taylfvallem1 23360 tayl0 23365 radcnvcl 23420 radcnvle 23423 psercnlem1 23428 eliccelico 28407 xrdifh 28410 unitssxrge0 28754 esumle 28927 esumlef 28931 esumpinfsum 28946 voliune 29100 volfiniune 29101 ddemeas 29107 prob01 29294 elicc3 31021 ftc1cnnclem 32059 ftc1anc 32069 ftc2nc 32070 iocinico 36140 icoiccdif 37662 iblsplit 37880 iblspltprt 37887 itgspltprt 37893 fourierdlem1 38007 iccpartrn 38781 |
Copyright terms: Public domain | W3C validator |