Theorem List for Intuitionistic Logic Explorer - 8901-9000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xneg11 8901 |
Extended real version of neg11 7359. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltnegi 8902 |
Forward direction of xltneg 8903. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xltneg 8903 |
Extended real version of ltneg 7566. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xleneg 8904 |
Extended real version of leneg 7569. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg1 8905 |
Extended real version of lt0neg1 7572. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xlt0neg2 8906 |
Extended real version of lt0neg2 7573. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xle0neg1 8907 |
Extended real version of le0neg1 7574. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xle0neg2 8908 |
Extended real version of le0neg2 7575. (Contributed by Mario Carneiro,
9-Sep-2015.)
|
|
|
Theorem | xnegcld 8909 |
Closure of extended real negative. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | xrex 8910 |
The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|
|
|
3.5.3 Real number intervals
|
|
Syntax | cioo 8911 |
Extend class notation with the set of open intervals of extended reals.
|
|
|
Syntax | cioc 8912 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
|
|
Syntax | cico 8913 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
|
|
Syntax | cicc 8914 |
Extend class notation with the set of closed intervals of extended
reals.
|
|
|
Definition | df-ioo 8915* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
|
|
Definition | df-ioc 8916* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
|
|
Definition | df-ico 8917* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
|
|
Definition | df-icc 8918* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
|
|
Theorem | ixxval 8919* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
|
|
Theorem | elixx1 8920* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
|
|
Theorem | ixxf 8921* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
|
|
Theorem | ixxex 8922* |
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
|
|
Theorem | ixxssxr 8923* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
|
|
Theorem | elixx3g 8924* |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
and .
(Contributed by Mario Carneiro,
3-Nov-2013.)
|
|
|
Theorem | ixxssixx 8925* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | ixxdisj 8926* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
|
|
Theorem | ixxss1 8927* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
|
|
Theorem | ixxss2 8928* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
|
|
Theorem | ixxss12 8929* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
|
|
Theorem | iooex 8930 |
The set of open intervals of extended reals exists. (Contributed by NM,
6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iooval 8931* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iooidg 8932 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
|
|
Theorem | elioo3g 8933 |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
and .
(Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | elioo1 8934 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | elioore 8935 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | lbioog 8936 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
|
|
Theorem | ubioog 8937 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
|
|
Theorem | iooval2 8938* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iooss1 8939 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
|
|
Theorem | iooss2 8940 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iocval 8941* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | icoval 8942* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iccval 8943* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | elioo2 8944 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | elioc1 8945 |
Membership in an open-below, closed-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
|
|
Theorem | elico1 8946 |
Membership in a closed-below, open-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
|
|
Theorem | elicc1 8947 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
|
|
Theorem | iccid 8948 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
|
|
Theorem | icc0r 8949 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
|
|
Theorem | eliooxr 8950 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
|
|
Theorem | eliooord 8951 |
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|
|
|
Theorem | ubioc1 8952 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 9007. (Contributed by FL, 29-May-2014.)
|
|
|
Theorem | lbico1 8953 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 9006. (Contributed by FL, 29-May-2014.)
|
|
|
Theorem | iccleub 8954 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
|
|
Theorem | iccgelb 8955 |
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23-Dec-2016.)
|
|
|
Theorem | elioo5 8956 |
Membership in an open interval of extended reals. (Contributed by NM,
17-Aug-2008.)
|
|
|
Theorem | elioo4g 8957 |
Membership in an open interval of extended reals. (Contributed by NM,
8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
|
|
Theorem | ioossre 8958 |
An open interval is a set of reals. (Contributed by NM,
31-May-2007.)
|
|
|
Theorem | elioc2 8959 |
Membership in an open-below, closed-above real interval. (Contributed by
Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
|
|
Theorem | elico2 8960 |
Membership in a closed-below, open-above real interval. (Contributed by
Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
|
|
Theorem | elicc2 8961 |
Membership in a closed real interval. (Contributed by Paul Chapman,
21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
|
|
Theorem | elicc2i 8962 |
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3-Jun-2013.)
|
|
|
Theorem | elicc4 8963 |
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|
|
|
Theorem | iccss 8964 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 20-Feb-2015.)
|
|
|
Theorem | iccssioo 8965 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
|
|
Theorem | icossico 8966 |
Condition for a closed-below, open-above interval to be a subset of a
closed-below, open-above interval. (Contributed by Thierry Arnoux,
21-Sep-2017.)
|
|
|
Theorem | iccss2 8967 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 28-Apr-2015.)
|
|
|
Theorem | iccssico 8968 |
Condition for a closed interval to be a subset of a half-open interval.
(Contributed by Mario Carneiro, 9-Sep-2015.)
|
|
|
Theorem | iccssioo2 8969 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
|
|
Theorem | iccssico2 8970 |
Condition for a closed interval to be a subset of a closed-below,
open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|
|
|
Theorem | ioomax 8971 |
The open interval from minus to plus infinity. (Contributed by NM,
6-Feb-2007.)
|
|
|
Theorem | iccmax 8972 |
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4-Jul-2014.)
|
|
|
Theorem | ioopos 8973 |
The set of positive reals expressed as an open interval. (Contributed by
NM, 7-May-2007.)
|
|
|
Theorem | ioorp 8974 |
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
|
|
Theorem | iooshf 8975 |
Shift the arguments of the open interval function. (Contributed by NM,
17-Aug-2008.)
|
|
|
Theorem | iocssre 8976 |
A closed-above interval with real upper bound is a set of reals.
(Contributed by FL, 29-May-2014.)
|
|
|
Theorem | icossre 8977 |
A closed-below interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
|
|
Theorem | iccssre 8978 |
A closed real interval is a set of reals. (Contributed by FL,
6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|
|
|
Theorem | iccssxr 8979 |
A closed interval is a set of extended reals. (Contributed by FL,
28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|
|
|
Theorem | iocssxr 8980 |
An open-below, closed-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
|
|
Theorem | icossxr 8981 |
A closed-below, open-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
|
|
Theorem | ioossicc 8982 |
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18-Oct-2007.)
|
|
|
Theorem | icossicc 8983 |
A closed-below, open-above interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25-Oct-2016.)
|
|
|
Theorem | iocssicc 8984 |
A closed-above, open-below interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1-Apr-2017.)
|
|
|
Theorem | ioossico 8985 |
An open interval is a subset of its closure-below. (Contributed by
Thierry Arnoux, 3-Mar-2017.)
|
|
|
Theorem | iocssioo 8986 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
|
|
Theorem | icossioo 8987 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
|
|
Theorem | ioossioo 8988 |
Condition for an open interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 26-Sep-2017.)
|
|
|
Theorem | iccsupr 8989* |
A nonempty subset of a closed real interval satisfies the conditions for
the existence of its supremum. To be useful without excluded middle,
we'll probably need to change not equal to apart, and perhaps make other
changes, but the theorem does hold as stated here. (Contributed by Paul
Chapman, 21-Jan-2008.)
|
|
|
Theorem | elioopnf 8990 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
|
|
Theorem | elioomnf 8991 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
|
|
Theorem | elicopnf 8992 |
Membership in a closed unbounded interval of reals. (Contributed by
Mario Carneiro, 16-Sep-2014.)
|
|
|
Theorem | repos 8993 |
Two ways of saying that a real number is positive. (Contributed by NM,
7-May-2007.)
|
|
|
Theorem | ioof 8994 |
The set of open intervals of extended reals maps to subsets of reals.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
|
|
Theorem | iccf 8995 |
The set of closed intervals of extended reals maps to subsets of
extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario
Carneiro, 3-Nov-2013.)
|
|
|
Theorem | unirnioo 8996 |
The union of the range of the open interval function. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|
|
|
Theorem | dfioo2 8997* |
Alternate definition of the set of open intervals of extended reals.
(Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro,
1-Sep-2015.)
|
|
|
Theorem | ioorebasg 8998 |
Open intervals are elements of the set of all open intervals.
(Contributed by Jim Kingdon, 4-Apr-2020.)
|
|
|
Theorem | elrege0 8999 |
The predicate "is a nonnegative real". (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|
|
|
Theorem | rge0ssre 9000 |
Nonnegative real numbers are real numbers. (Contributed by Thierry
Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
|
|