Type  Label  Description 
Statement 

Theorem  xrnepnf 8801 
An extended real other than plus infinity is real or negative infinite.
(Contributed by Mario Carneiro, 20Aug2015.)



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



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



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



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



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



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



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



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



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



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



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



Theorem  nn0pnfge0 8813 
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 8814 
Minus infinity is less than or equal to any extended real. (Contributed
by NM, 19Jan2006.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



3.5.3 Real number intervals


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

