![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elioo2 | Structured version Visualization version Unicode version |
Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
Ref | Expression |
---|---|
elioo2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iooval2 11658 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq2d 2514 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | breq2 4377 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | breq1 4376 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | anbi12d 722 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | elrab 3163 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3anass 990 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 6, 7 | bitr4i 260 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2, 8 | syl6bb 269 |
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 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-cnex 9581 ax-resscn 9582 ax-pre-lttri 9599 ax-pre-lttrn 9600 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3014 df-sbc 3235 df-csb 3331 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-op 3942 df-uni 4168 df-iun 4249 df-br 4374 df-opab 4433 df-mpt 4434 df-id 4726 df-po 4732 df-so 4733 df-xp 4817 df-rel 4818 df-cnv 4819 df-co 4820 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 df-iota 5524 df-fun 5562 df-fn 5563 df-f 5564 df-f1 5565 df-fo 5566 df-f1o 5567 df-fv 5568 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-1st 6780 df-2nd 6781 df-er 7349 df-en 7556 df-dom 7557 df-sdom 7558 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 df-ioo 11628 |
This theorem is referenced by: eliooord 11683 elioopnf 11717 elioomnf 11718 difreicc 11754 xov1plusxeqvd 11768 tanhbnd 14225 bl2ioo 21820 xrtgioo 21834 zcld 21841 iccntr 21849 icccmplem2 21851 reconnlem1 21854 reconnlem2 21855 icoopnst 21977 iocopnst 21978 ivthlem3 22414 ovolicc2lem1 22480 ovolicc2lem5 22485 ioombl1lem4 22525 mbfmax 22616 itg2monolem1 22719 itg2monolem3 22721 dvferm1lem 22947 dvferm2lem 22949 dvlip2 22958 dvivthlem1 22971 lhop1lem 22976 lhop 22979 dvcnvrelem1 22980 dvcnvre 22982 itgsubst 23012 sincosq1sgn 23464 sincosq2sgn 23465 sincosq3sgn 23466 sincosq4sgn 23467 coseq00topi 23468 tanabsge 23472 sinq12gt0 23473 sinq12ge0 23474 cosq14gt0 23476 sincos6thpi 23481 sineq0 23487 cosordlem 23491 tanord1 23497 tanord 23498 argregt0 23570 argimgt0 23572 argimlt0 23573 dvloglem 23604 logf1o2 23606 efopnlem2 23613 asinsinlem 23828 acoscos 23830 atanlogsublem 23852 atantan 23860 atanbndlem 23862 atanbnd 23863 atan1 23865 scvxcvx 23922 basellem1 24018 pntibndlem1 24438 pntibnd 24442 pntlemc 24444 padicabvf 24480 padicabvcxp 24481 dfrp2 28359 cnre2csqlem 28722 ivthALT 30996 iooelexlt 31766 dvtanlemOLD 31992 itg2gt0cn 31998 iblabsnclem 32006 dvasin 32029 areacirclem1 32033 areacirc 32038 cvgdvgrat 36662 radcnvrat 36663 sineq0ALT 37330 ioogtlb 37632 eliood 37635 eliooshift 37644 iooltub 37650 limciccioolb 37742 limcicciooub 37758 cncfioobdlem 37815 ditgeqiooicc 37878 dirkercncflem1 38021 dirkercncflem4 38024 fourierdlem10 38035 fourierdlem32 38058 fourierdlem62 38088 fourierdlem81 38107 fourierdlem82 38108 fourierdlem93 38119 fourierdlem104 38130 fourierdlem111 38137 |
Copyright terms: Public domain | W3C validator |