Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  iccf 8571 
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 8572 
The union of the range of the open interval function. (Contributed by
NM, 7May2007.) (Revised by Mario Carneiro, 30Jan2014.)



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



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



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



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



Theorem  elxrge0 8577 
Elementhood in the set of nonnegative extended reals. (Contributed by
Mario Carneiro, 28Jun2014.)



Theorem  0e0icopnf 8578 
0 is a member of
(common case). (Contributed by David
A. Wheeler, 8Dec2018.)



Theorem  0e0iccpnf 8579 
0 is a member of
(common case). (Contributed by David
A. Wheeler, 8Dec2018.)



Theorem  ge0addcl 8580 
The nonnegative reals are closed under addition. (Contributed by Mario
Carneiro, 19Jun2014.)



Theorem  ge0mulcl 8581 
The nonnegative reals are closed under multiplication. (Contributed by
Mario Carneiro, 19Jun2014.)



Theorem  lbicc2 8582 
The lower bound of a closed interval is a member of it. (Contributed by
Paul Chapman, 26Nov2007.) (Revised by FL, 29May2014.) (Revised by
Mario Carneiro, 9Sep2015.)



Theorem  ubicc2 8583 
The upper bound of a closed interval is a member of it. (Contributed by
Paul Chapman, 26Nov2007.) (Revised by FL, 29May2014.)



Theorem  0elunit 8584 
Zero is an element of the closed unit. (Contributed by Scott Fenton,
11Jun2013.)



Theorem  1elunit 8585 
One is an element of the closed unit. (Contributed by Scott Fenton,
11Jun2013.)



Theorem  iooneg 8586 
Membership in a negated open real interval. (Contributed by Paul Chapman,
26Nov2007.)



Theorem  iccneg 8587 
Membership in a negated closed real interval. (Contributed by Paul
Chapman, 26Nov2007.)



Theorem  icoshft 8588 
A shifted real is a member of a shifted, closedbelow, openabove real
interval. (Contributed by Paul Chapman, 25Mar2008.)



Theorem  icoshftf1o 8589* 
Shifting a closedbelow, openabove interval is onetoone onto.
(Contributed by Paul Chapman, 25Mar2008.) (Proof shortened by Mario
Carneiro, 1Sep2015.)



Theorem  icodisj 8590 
Endtoend closedbelow, openabove real intervals are disjoint.
(Contributed by Mario Carneiro, 16Jun2014.)



Theorem  ioodisj 8591 
If the upper bound of one open interval is less than or equal to the
lower bound of the other, the intervals are disjoint. (Contributed by
Jeff Hankins, 13Jul2009.)



Theorem  iccshftr 8592 
Membership in a shifted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iccshftri 8593 
Membership in a shifted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iccshftl 8594 
Membership in a shifted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iccshftli 8595 
Membership in a shifted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iccdil 8596 
Membership in a dilated interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  iccdili 8597 
Membership in a dilated interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  icccntr 8598 
Membership in a contracted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  icccntri 8599 
Membership in a contracted interval. (Contributed by Jeff Madsen,
2Sep2009.)



Theorem  divelunit 8600 
A condition for a ratio to be a member of the closed unit. (Contributed
by Scott Fenton, 11Jun2013.)

