Type  Label  Description 
Statement 

Theorem  ngtmnft 8501 
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2Feb2006.)



Theorem  xrrebnd 8502 
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2Feb2006.)



Theorem  xrre 8503 
A way of proving that an extended real is real. (Contributed by NM,
9Mar2006.)



Theorem  xrre2 8504 
An extended real between two others is real. (Contributed by NM,
6Feb2007.)



Theorem  xrre3 8505 
A way of proving that an extended real is real. (Contributed by FL,
29May2014.)



Theorem  ge0gtmnf 8506 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  ge0nemnf 8507 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xrrege0 8508 
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  z2ge 8509* 
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28Aug2005.)



Theorem  xnegeq 8510 
Equality of two extended numbers with in front of them.
(Contributed by FL, 26Dec2011.) (Proof shortened by Mario Carneiro,
20Aug2015.)



Theorem  xnegpnf 8511 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.)



Theorem  xnegmnf 8512 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.) (Revised by Mario Carneiro, 20Aug2015.)



Theorem  rexneg 8513 
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26Dec2011.) (Proof shortened by Mario Carneiro, 20Aug2015.)



Theorem  xneg0 8514 
The negative of zero. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xnegcl 8515 
Closure of extended real negative. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xnegneg 8516 
Extended real version of negneg 7057. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xneg11 8517 
Extended real version of neg11 7058. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltnegi 8518 
Forward direction of xltneg 8519. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltneg 8519 
Extended real version of ltneg 7252. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleneg 8520 
Extended real version of leneg 7255. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg1 8521 
Extended real version of lt0neg1 7258. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg2 8522 
Extended real version of lt0neg2 7259. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xle0neg1 8523 
Extended real version of le0neg1 7260. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xle0neg2 8524 
Extended real version of le0neg2 7261. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xnegcld 8525 
Closure of extended real negative. (Contributed by Mario Carneiro,
28May2016.)



Theorem  xrex 8526 
The set of extended reals exists. (Contributed by NM, 24Dec2006.)



3.5.3 Real number intervals


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

