Type  Label  Description 
Statement 

Theorem  xaddge0 9601 
The sum of nonnegative extended reals is nonnegative. (Contributed by
Mario Carneiro, 21Aug2015.)



Theorem  xle2add 9602 
Extended real version of le2add 8170. (Contributed by Mario Carneiro,
23Aug2015.)



Theorem  xlt2add 9603 
Extended real version of lt2add 8171. Note that ltleadd 8172, which has
weaker assumptions, is not true for the extended reals (since
fails). (Contributed by Mario
Carneiro,
23Aug2015.)



Theorem  xsubge0 9604 
Extended real version of subge0 8201. (Contributed by Mario Carneiro,
24Aug2015.)



Theorem  xposdif 9605 
Extended real version of posdif 8181. (Contributed by Mario Carneiro,
24Aug2015.) (Revised by Jim Kingdon, 17Apr2023.)



Theorem  xlesubadd 9606 
Under certain conditions, the conclusion of lesubadd 8160 is true even in the
extended reals. (Contributed by Mario Carneiro, 4Sep2015.)



Theorem  xaddcld 9607 
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  xadd4d 9608 
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 7895. (Contributed by Alexander van der Vekens,
21Dec2017.)



Theorem  xnn0add4d 9609 
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9608. (Contributed by AV,
12Dec2020.)

NN0* NN0* NN0* NN0* 

Theorem  xleaddadd 9610 
Cancelling a factor of two in (expressed as addition rather than
as a factor to avoid extended real multiplication). (Contributed by Jim
Kingdon, 18Apr2023.)



4.5.3 Real number intervals


Syntax  cioo 9611 
Extend class notation with the set of open intervals of extended reals.



Syntax  cioc 9612 
Extend class notation with the set of openbelow, closedabove intervals
of extended reals.



Syntax  cico 9613 
Extend class notation with the set of closedbelow, openabove intervals
of extended reals.



Syntax  cicc 9614 
Extend class notation with the set of closed intervals of extended
reals.



Definition  dfioo 9615* 
Define the set of open intervals of extended reals. (Contributed by NM,
24Dec2006.)



Definition  dfioc 9616* 
Define the set of openbelow, closedabove intervals of extended reals.
(Contributed by NM, 24Dec2006.)



Definition  dfico 9617* 
Define the set of closedbelow, openabove intervals of extended reals.
(Contributed by NM, 24Dec2006.)



Definition  dficc 9618* 
Define the set of closed intervals of extended reals. (Contributed by
NM, 24Dec2006.)



Theorem  ixxval 9619* 
Value of the interval function. (Contributed by Mario Carneiro,
3Nov2013.)



Theorem  elixx1 9620* 
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3Nov2013.)



Theorem  ixxf 9621* 
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by FL, 14Jun2007.) (Revised by Mario Carneiro,
16Nov2013.)



Theorem  ixxex 9622* 
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3Nov2013.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  ixxssxr 9623* 
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4Jul2014.)



Theorem  elixx3g 9624* 
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,
3Nov2013.)



Theorem  ixxssixx 9625* 
An interval is a subset of its closure. (Contributed by Paul Chapman,
18Oct2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  ixxdisj 9626* 
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16Jun2014.)



Theorem  ixxss1 9627* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3Nov2013.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  ixxss2 9628* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3Nov2013.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  ixxss12 9629* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20Feb2015.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  iooex 9630 
The set of open intervals of extended reals exists. (Contributed by NM,
6Feb2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooval 9631* 
Value of the open interval function. (Contributed by NM, 24Dec2006.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooidg 9632 
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29Mar2020.)



Theorem  elioo3g 9633 
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, 24Dec2006.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioo1 9634 
Membership in an open interval of extended reals. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioore 9635 
A member of an open interval of reals is a real. (Contributed by NM,
17Aug2008.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  lbioog 9636 
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30Mar2020.)



Theorem  ubioog 9637 
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30Mar2020.)



Theorem  iooval2 9638* 
Value of the open interval function. (Contributed by NM, 6Feb2007.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooss1 9639 
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7Feb2007.) (Revised by Mario Carneiro, 20Feb2015.)



Theorem  iooss2 9640 
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7Feb2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iocval 9641* 
Value of the openbelow, closedabove interval function. (Contributed
by NM, 24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  icoval 9642* 
Value of the closedbelow, openabove interval function. (Contributed
by NM, 24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iccval 9643* 
Value of the closed interval function. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioo2 9644 
Membership in an open interval of extended reals. (Contributed by NM,
6Feb2007.)



Theorem  elioc1 9645 
Membership in an openbelow, closedabove interval of extended reals.
(Contributed by NM, 24Dec2006.) (Revised by Mario Carneiro,
3Nov2013.)



Theorem  elico1 9646 
Membership in a closedbelow, openabove interval of extended reals.
(Contributed by NM, 24Dec2006.) (Revised by Mario Carneiro,
3Nov2013.)



Theorem  elicc1 9647 
Membership in a closed interval of extended reals. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iccid 9648 
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13Jul2009.)



Theorem  icc0r 9649 
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30Mar2020.)



Theorem  eliooxr 9650 
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17Aug2008.)



Theorem  eliooord 9651 
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17Aug2008.) (Revised by Mario Carneiro, 9May2014.)



Theorem  ubioc1 9652 
The upper bound belongs to an openbelow, closedabove interval. See
ubicc2 9708. (Contributed by FL, 29May2014.)



Theorem  lbico1 9653 
The lower bound belongs to a closedbelow, openabove interval. See
lbicc2 9707. (Contributed by FL, 29May2014.)



Theorem  iccleub 9654 
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14Jul2009.)



Theorem  iccgelb 9655 
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23Dec2016.)



Theorem  elioo5 9656 
Membership in an open interval of extended reals. (Contributed by NM,
17Aug2008.)



Theorem  elioo4g 9657 
Membership in an open interval of extended reals. (Contributed by NM,
8Jun2007.) (Revised by Mario Carneiro, 28Apr2015.)



Theorem  ioossre 9658 
An open interval is a set of reals. (Contributed by NM,
31May2007.)



Theorem  elioc2 9659 
Membership in an openbelow, closedabove real interval. (Contributed by
Paul Chapman, 30Dec2007.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elico2 9660 
Membership in a closedbelow, openabove real interval. (Contributed by
Paul Chapman, 21Jan2008.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elicc2 9661 
Membership in a closed real interval. (Contributed by Paul Chapman,
21Sep2007.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elicc2i 9662 
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3Jun2013.)



Theorem  elicc4 9663 
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16Nov2014.) (Proof shortened by Mario Carneiro, 1Jan2017.)



Theorem  iccss 9664 
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 20Feb2015.)



Theorem  iccssioo 9665 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20Feb2015.)



Theorem  icossico 9666 
Condition for a closedbelow, openabove interval to be a subset of a
closedbelow, openabove interval. (Contributed by Thierry Arnoux,
21Sep2017.)



Theorem  iccss2 9667 
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 28Apr2015.)



Theorem  iccssico 9668 
Condition for a closed interval to be a subset of a halfopen interval.
(Contributed by Mario Carneiro, 9Sep2015.)



Theorem  iccssioo2 9669 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20Feb2015.)



Theorem  iccssico2 9670 
Condition for a closed interval to be a subset of a closedbelow,
openabove interval. (Contributed by Mario Carneiro, 20Feb2015.)



Theorem  ioomax 9671 
The open interval from minus to plus infinity. (Contributed by NM,
6Feb2007.)



Theorem  iccmax 9672 
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4Jul2014.)



Theorem  ioopos 9673 
The set of positive reals expressed as an open interval. (Contributed by
NM, 7May2007.)



Theorem  ioorp 9674 
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25Nov2007.)



Theorem  iooshf 9675 
Shift the arguments of the open interval function. (Contributed by NM,
17Aug2008.)



Theorem  iocssre 9676 
A closedabove interval with real upper bound is a set of reals.
(Contributed by FL, 29May2014.)



Theorem  icossre 9677 
A closedbelow interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14Jun2014.)



Theorem  iccssre 9678 
A closed real interval is a set of reals. (Contributed by FL,
6Jun2007.) (Proof shortened by Paul Chapman, 21Jan2008.)



Theorem  iccssxr 9679 
A closed interval is a set of extended reals. (Contributed by FL,
28Jul2008.) (Revised by Mario Carneiro, 4Jul2014.)



Theorem  iocssxr 9680 
An openbelow, closedabove interval is a subset of the extended reals.
(Contributed by FL, 29May2014.) (Revised by Mario Carneiro,
4Jul2014.)



Theorem  icossxr 9681 
A closedbelow, openabove interval is a subset of the extended reals.
(Contributed by FL, 29May2014.) (Revised by Mario Carneiro,
4Jul2014.)



Theorem  ioossicc 9682 
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18Oct2007.)



Theorem  icossicc 9683 
A closedbelow, openabove interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25Oct2016.)



Theorem  iocssicc 9684 
A closedabove, openbelow interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1Apr2017.)



Theorem  ioossico 9685 
An open interval is a subset of its closurebelow. (Contributed by
Thierry Arnoux, 3Mar2017.)



Theorem  iocssioo 9686 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29Mar2017.)



Theorem  icossioo 9687 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29Mar2017.)



Theorem  ioossioo 9688 
Condition for an open interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 26Sep2017.)



Theorem  iccsupr 9689* 
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, 21Jan2008.)



Theorem  elioopnf 9690 
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18Jun2014.)



Theorem  elioomnf 9691 
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18Jun2014.)



Theorem  elicopnf 9692 
Membership in a closed unbounded interval of reals. (Contributed by
Mario Carneiro, 16Sep2014.)



Theorem  repos 9693 
Two ways of saying that a real number is positive. (Contributed by NM,
7May2007.)



Theorem  ioof 9694 
The set of open intervals of extended reals maps to subsets of reals.
(Contributed by NM, 7Feb2007.) (Revised by Mario Carneiro,
16Nov2013.)



Theorem  iccf 9695 
The set of closed intervals of extended reals maps to subsets of
extended reals. (Contributed by FL, 14Jun2007.) (Revised by Mario
Carneiro, 3Nov2013.)



Theorem  unirnioo 9696 
The union of the range of the open interval function. (Contributed by
NM, 7May2007.) (Revised by Mario Carneiro, 30Jan2014.)



Theorem  dfioo2 9697* 
Alternate definition of the set of open intervals of extended reals.
(Contributed by NM, 1Mar2007.) (Revised by Mario Carneiro,
1Sep2015.)



Theorem  ioorebasg 9698 
Open intervals are elements of the set of all open intervals.
(Contributed by Jim Kingdon, 4Apr2020.)



Theorem  elrege0 9699 
The predicate "is a nonnegative real". (Contributed by Jeff Madsen,
2Sep2009.) (Proof shortened by Mario Carneiro, 18Jun2014.)



Theorem  rge0ssre 9700 
Nonnegative real numbers are real numbers. (Contributed by Thierry
Arnoux, 9Sep2018.) (Proof shortened by AV, 8Sep2019.)

