Type  Label  Description 
Statement 

Theorem  xnegdi 9701 
Extended real version of negdi 8063. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xaddass 9702 
Associativity of extended real addition. The correct condition here is
"it is not the case that both and appear as one of
,
i.e. ", but this
condition is difficult to work with, so we break the theorem into two
parts: this one, where is not present in , and
xaddass2 9703, where is not present. (Contributed by Mario
Carneiro, 20Aug2015.)



Theorem  xaddass2 9703 
Associativity of extended real addition. See xaddass 9702 for notes on the
hypotheses. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xpncan 9704 
Extended real version of pncan 8012. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xnpcan 9705 
Extended real version of npcan 8015. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd1a 9706 
Extended real version of leadd1 8236; note that the converse implication is
not true, unlike the real version (for example but
).
(Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd2a 9707 
Commuted form of xleadd1a 9706. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleadd1 9708 
Weakened version of xleadd1a 9706 under which the reverse implication is
true. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xltadd1 9709 
Extended real version of ltadd1 8235. (Contributed by Mario Carneiro,
23Aug2015.) (Revised by Jim Kingdon, 16Apr2023.)



Theorem  xltadd2 9710 
Extended real version of ltadd2 8225. (Contributed by Mario Carneiro,
23Aug2015.)



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



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



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



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



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



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



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



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



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

NN0* NN0* NN0* NN0* 

Theorem  xleaddadd 9720 
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 9721 
Extend class notation with the set of open intervals of extended reals.



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  elixx3g 9734* 
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 9735* 
An interval is a subset of its closure. (Contributed by Paul Chapman,
18Oct2007.) (Revised by Mario Carneiro, 3Nov2013.)



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



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



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



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



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



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



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



Theorem  elioo3g 9743 
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 9744 
Membership in an open interval of extended reals. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  iccss 9774 
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 9775 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20Feb2015.)



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



Theorem  iccss2 9777 
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 9778 
Condition for a closed interval to be a subset of a halfopen interval.
(Contributed by Mario Carneiro, 9Sep2015.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  iccsupr 9799* 
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 9800 
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18Jun2014.)

