Type  Label  Description 
Statement 

Theorem  xrltnr 8701 
The extended real 'less than' is irreflexive. (Contributed by NM,
14Oct2005.)



Theorem  ltpnf 8702 
Any (finite) real is less than plus infinity. (Contributed by NM,
14Oct2005.)



Theorem  0ltpnf 8703 
Zero is less than plus infinity (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  mnflt 8704 
Minus infinity is less than any (finite) real. (Contributed by NM,
14Oct2005.)



Theorem  mnflt0 8705 
Minus infinity is less than 0 (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  mnfltpnf 8706 
Minus infinity is less than plus infinity. (Contributed by NM,
14Oct2005.)



Theorem  mnfltxr 8707 
Minus infinity is less than an extended real that is either real or plus
infinity. (Contributed by NM, 2Feb2006.)



Theorem  pnfnlt 8708 
No extended real is greater than plus infinity. (Contributed by NM,
15Oct2005.)



Theorem  nltmnf 8709 
No extended real is less than minus infinity. (Contributed by NM,
15Oct2005.)



Theorem  pnfge 8710 
Plus infinity is an upper bound for extended reals. (Contributed by NM,
30Jan2006.)



Theorem  0lepnf 8711 
0 less than or equal to positive infinity. (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  nn0pnfge0 8712 
If a number is a nonnegative integer or positive infinity, it is greater
than or equal to 0. (Contributed by Alexander van der Vekens,
6Jan2018.)



Theorem  mnfle 8713 
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19Jan2006.)



Theorem  xrltnsym 8714 
Ordering on the extended reals is not symmetric. (Contributed by NM,
15Oct2005.)



Theorem  xrltnsym2 8715 
'Less than' is antisymmetric and irreflexive for extended reals.
(Contributed by NM, 6Feb2007.)



Theorem  xrlttr 8716 
Ordering on the extended reals is transitive. (Contributed by NM,
15Oct2005.)



Theorem  xrltso 8717 
'Less than' is a weakly linear ordering on the extended reals.
(Contributed by NM, 15Oct2005.)



Theorem  xrlttri3 8718 
Extended real version of lttri3 7098. (Contributed by NM, 9Feb2006.)



Theorem  xrltle 8719 
'Less than' implies 'less than or equal' for extended reals. (Contributed
by NM, 19Jan2006.)



Theorem  xrleid 8720 
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7Feb2007.)



Theorem  xrletri3 8721 
Trichotomy law for extended reals. (Contributed by FL, 2Aug2009.)



Theorem  xrlelttr 8722 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrltletr 8723 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrletr 8724 
Transitive law for ordering on extended reals. (Contributed by NM,
9Feb2006.)



Theorem  xrlttrd 8725 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrlelttrd 8726 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltletrd 8727 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrletrd 8728 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltne 8729 
'Less than' implies not equal for extended reals. (Contributed by NM,
20Jan2006.)



Theorem  nltpnft 8730 
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30Jan2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



3.5.3 Real number intervals


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

