Type  Label  Description 
Statement 

Theorem  absnegd 10801 
Absolute value of negative. (Contributed by Mario Carneiro,
29May2016.)



Theorem  abscjd 10802 
The absolute value of a number and its conjugate are the same.
Proposition 103.7(b) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29May2016.)



Theorem  releabsd 10803 
The real part of a number is less than or equal to its absolute value.
Proposition 103.7(d) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29May2016.)



Theorem  absexpd 10804 
Absolute value of positive integer exponentiation. (Contributed by
Mario Carneiro, 29May2016.)



Theorem  abssubd 10805 
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by Mario Carneiro,
29May2016.)



Theorem  absmuld 10806 
Absolute value distributes over multiplication. Proposition 103.7(f)
of [Gleason] p. 133. (Contributed by
Mario Carneiro, 29May2016.)



Theorem  absdivapd 10807 
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13Aug2021.)

#


Theorem  abstrid 10808 
Triangle inequality for absolute value. Proposition 103.7(h) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29May2016.)



Theorem  abs2difd 10809 
Difference of absolute values. (Contributed by Mario Carneiro,
29May2016.)



Theorem  abs2dif2d 10810 
Difference of absolute values. (Contributed by Mario Carneiro,
29May2016.)



Theorem  abs2difabsd 10811 
Absolute value of difference of absolute values. (Contributed by Mario
Carneiro, 29May2016.)



Theorem  abs3difd 10812 
Absolute value of differences around common element. (Contributed by
Mario Carneiro, 29May2016.)



Theorem  abs3lemd 10813 
Lemma involving absolute value of differences. (Contributed by Mario
Carneiro, 29May2016.)



Theorem  qdenre 10814* 
The rational numbers are dense in : any real number can be
approximated with arbitrary precision by a rational number. For order
theoretic density, see qbtwnre 9875. (Contributed by BJ, 15Oct2021.)



3.7.5 The maximum of two real
numbers


Theorem  maxcom 10815 
The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10.
(Contributed by Jim Kingdon, 21Dec2021.)



Theorem  maxabsle 10816 
An upper bound for . (Contributed by Jim Kingdon,
20Dec2021.)



Theorem  maxleim 10817 
Value of maximum when we know which number is larger. (Contributed by
Jim Kingdon, 21Dec2021.)



Theorem  maxabslemab 10818 
Lemma for maxabs 10821. A variation of maxleim 10817 that is, if we know
which of two real numbers is larger, we know the maximum of the two.
(Contributed by Jim Kingdon, 21Dec2021.)



Theorem  maxabslemlub 10819 
Lemma for maxabs 10821. A least upper bound for .
(Contributed by Jim Kingdon, 20Dec2021.)



Theorem  maxabslemval 10820* 
Lemma for maxabs 10821. Value of the supremum. (Contributed by
Jim
Kingdon, 22Dec2021.)



Theorem  maxabs 10821 
Maximum of two real numbers in terms of absolute value. (Contributed by
Jim Kingdon, 20Dec2021.)



Theorem  maxcl 10822 
The maximum of two real numbers is a real number. (Contributed by Jim
Kingdon, 22Dec2021.)



Theorem  maxle1 10823 
The maximum of two reals is no smaller than the first real. Lemma 3.10 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 21Dec2021.)



Theorem  maxle2 10824 
The maximum of two reals is no smaller than the second real. Lemma 3.10
of [Geuvers], p. 10. (Contributed by Jim
Kingdon, 21Dec2021.)



Theorem  maxleast 10825 
The maximum of two reals is a least upper bound. Lemma 3.11 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 22Dec2021.)



Theorem  maxleastb 10826 
Two ways of saying the maximum of two numbers is less than or equal to a
third. (Contributed by Jim Kingdon, 31Jan2022.)



Theorem  maxleastlt 10827 
The maximum as a least upper bound, in terms of less than. (Contributed
by Jim Kingdon, 9Feb2022.)



Theorem  maxleb 10828 
Equivalence of
and being equal to the maximum of two reals. Lemma
3.12 of [Geuvers], p. 10. (Contributed by
Jim Kingdon, 21Dec2021.)



Theorem  dfabsmax 10829 
Absolute value of a real number in terms of maximum. Definition 3.13 of
[Geuvers], p. 11. (Contributed by BJ and
Jim Kingdon, 21Dec2021.)



Theorem  maxltsup 10830 
Two ways of saying the maximum of two numbers is less than a third.
(Contributed by Jim Kingdon, 10Feb2022.)



Theorem  max0addsup 10831 
The sum of the positive and negative part functions is the absolute value
function over the reals. (Contributed by Jim Kingdon, 30Jan2022.)



Theorem  rexanre 10832* 
Combine two different upper real properties into one. (Contributed by
Mario Carneiro, 8May2016.)



Theorem  rexico 10833* 
Restrict the base of an upper real quantifier to an upper real set.
(Contributed by Mario Carneiro, 12May2016.)



Theorem  maxclpr 10834 
The maximum of two real numbers is one of those numbers if and only if
dichotomy (
) holds. For example, this
can be
combined with zletric 8950 if one is dealing with integers, but real
number
dichotomy in general does not follow from our axioms. (Contributed by Jim
Kingdon, 1Feb2022.)



Theorem  zmaxcl 10835 
The maximum of two integers is an integer. (Contributed by Jim Kingdon,
27Sep2022.)



Theorem  2zsupmax 10836 
Two ways to express the maximum of two integers. Because order of
integers is decidable, we have more flexibility than for real numbers.
(Contributed by Jim Kingdon, 22Jan2023.)



Theorem  fimaxre2 10837* 
A nonempty finite set of real numbers has an upper bound. (Contributed
by Jeff Madsen, 27May2011.) (Revised by Mario Carneiro,
13Feb2014.)



Theorem  negfi 10838* 
The negation of a finite set of real numbers is finite. (Contributed by
AV, 9Aug2020.)



3.7.6 The minimum of two real
numbers


Theorem  mincom 10839 
The minimum of two reals is commutative. (Contributed by Jim Kingdon,
8Feb2021.)

inf inf


Theorem  minmax 10840 
Minimum expressed in terms of maximum. (Contributed by Jim Kingdon,
8Feb2021.)

inf 

Theorem  mincl 10841 
The minumum of two real numbers is a real number. (Contributed by Jim
Kingdon, 25Apr2023.)

inf 

Theorem  min1inf 10842 
The minimum of two numbers is less than or equal to the first.
(Contributed by Jim Kingdon, 8Feb2021.)

inf 

Theorem  min2inf 10843 
The minimum of two numbers is less than or equal to the second.
(Contributed by Jim Kingdon, 9Feb2021.)

inf 

Theorem  lemininf 10844 
Two ways of saying a number is less than or equal to the minimum of two
others. (Contributed by NM, 3Aug2007.)

inf


Theorem  ltmininf 10845 
Two ways of saying a number is less than the minimum of two others.
(Contributed by Jim Kingdon, 10Feb2022.)

inf 

Theorem  minabs 10846 
The minimum of two real numbers in terms of absolute value. (Contributed
by Jim Kingdon, 15May2023.)

inf


Theorem  minclpr 10847 
The minimum of two real numbers is one of those numbers if and only if
dichotomy (
) holds. For example, this
can be
combined with zletric 8950 if one is dealing with integers, but real
number
dichotomy in general does not follow from our axioms. (Contributed by Jim
Kingdon, 23May2023.)

inf


Theorem  rpmincl 10848 
The minumum of two positive real numbers is a positive real number.
(Contributed by Jim Kingdon, 25Apr2023.)

inf 

Theorem  bdtrilem 10849 
Lemma for bdtri 10850. (Contributed by Steven Nguyen and Jim
Kingdon,
17May2023.)



Theorem  bdtri 10850 
Triangle inequality for bounded values. (Contributed by Jim Kingdon,
15May2023.)

inf
inf inf 

Theorem  mul0inf 10851 
Equality of a product with zero. A bit of a curiosity, in the sense that
theorems like abs00ap 10674 and mulap0bd 8279 may better express the ideas behind
it. (Contributed by Jim Kingdon, 31Jul2023.)

inf 

3.7.7 The maximum of two extended
reals


Theorem  xrmaxleim 10852 
Value of maximum when we know which extended real is larger.
(Contributed by Jim Kingdon, 25Apr2023.)



Theorem  xrmaxiflemcl 10853 
Lemma for xrmaxif 10859. Closure. (Contributed by Jim Kingdon,
29Apr2023.)



Theorem  xrmaxifle 10854 
An upper bound for in the extended reals. (Contributed by
Jim Kingdon, 26Apr2023.)



Theorem  xrmaxiflemab 10855 
Lemma for xrmaxif 10859. A variation of xrmaxleim 10852 that is, if we know
which of two real numbers is larger, we know the maximum of the two.
(Contributed by Jim Kingdon, 26Apr2023.)



Theorem  xrmaxiflemlub 10856 
Lemma for xrmaxif 10859. A least upper bound for .
(Contributed by Jim Kingdon, 28Apr2023.)



Theorem  xrmaxiflemcom 10857 
Lemma for xrmaxif 10859. Commutativity of an expression which we
will
later show to be the supremum. (Contributed by Jim Kingdon,
29Apr2023.)



Theorem  xrmaxiflemval 10858* 
Lemma for xrmaxif 10859. Value of the supremum. (Contributed by
Jim
Kingdon, 29Apr2023.)



Theorem  xrmaxif 10859 
Maximum of two extended reals in terms of expressions.
(Contributed by Jim Kingdon, 26Apr2023.)



Theorem  xrmaxcl 10860 
The maximum of two extended reals is an extended real. (Contributed by
Jim Kingdon, 29Apr2023.)



Theorem  xrmax1sup 10861 
An extended real is less than or equal to the maximum of it and another.
(Contributed by NM, 7Feb2007.) (Revised by Jim Kingdon,
30Apr2023.)



Theorem  xrmax2sup 10862 
An extended real is less than or equal to the maximum of it and another.
(Contributed by NM, 7Feb2007.) (Revised by Jim Kingdon,
30Apr2023.)



Theorem  xrmaxrecl 10863 
The maximum of two real numbers is the same when taken as extended reals
or as reals. (Contributed by Jim Kingdon, 30Apr2023.)



Theorem  xrmaxleastlt 10864 
The maximum as a least upper bound, in terms of less than. (Contributed
by Jim Kingdon, 9Feb2022.)



Theorem  xrltmaxsup 10865 
The maximum as a least upper bound. (Contributed by Jim Kingdon,
10May2023.)



Theorem  xrmaxltsup 10866 
Two ways of saying the maximum of two numbers is less than a third.
(Contributed by Jim Kingdon, 30Apr2023.)



Theorem  xrmaxlesup 10867 
Two ways of saying the maximum of two numbers is less than or equal to a
third. (Contributed by Mario Carneiro, 18Jun2014.) (Revised by Jim
Kingdon, 10May2023.)



Theorem  xrmaxaddlem 10868 
Lemma for xrmaxadd 10869. The case where is real. (Contributed by
Jim Kingdon, 11May2023.)



Theorem  xrmaxadd 10869 
Distributing addition over maximum. (Contributed by Jim Kingdon,
11May2023.)



3.7.8 The minimum of two extended
reals


Theorem  xrnegiso 10870 
Negation is an order antiisomorphism of the extended reals, which is
its own inverse. (Contributed by Jim Kingdon, 2May2023.)



Theorem  infxrnegsupex 10871* 
The infimum of a set of extended reals is the negative of the
supremum of the negatives of its elements. (Contributed by Jim Kingdon,
2May2023.)

inf


Theorem  xrnegcon1d 10872 
Contraposition law for extended real unary minus. (Contributed by Jim
Kingdon, 2May2023.)



Theorem  xrminmax 10873 
Minimum expressed in terms of maximum. (Contributed by Jim Kingdon,
2May2023.)

inf


Theorem  xrmincl 10874 
The minumum of two extended reals is an extended real. (Contributed by
Jim Kingdon, 3May2023.)

inf 

Theorem  xrmin1inf 10875 
The minimum of two extended reals is less than or equal to the first.
(Contributed by Jim Kingdon, 3May2023.)

inf 

Theorem  xrmin2inf 10876 
The minimum of two extended reals is less than or equal to the second.
(Contributed by Jim Kingdon, 3May2023.)

inf 

Theorem  xrmineqinf 10877 
The minimum of two extended reals is equal to the second if the first is
bigger. (Contributed by Mario Carneiro, 25Mar2015.) (Revised by Jim
Kingdon, 3May2023.)

inf


Theorem  xrltmininf 10878 
Two ways of saying an extended real is less than the minimum of two
others. (Contributed by NM, 7Feb2007.) (Revised by Jim Kingdon,
3May2023.)

inf 

Theorem  xrlemininf 10879 
Two ways of saying a number is less than or equal to the minimum of two
others. (Contributed by Mario Carneiro, 18Jun2014.) (Revised by Jim
Kingdon, 4May2023.)

inf 

Theorem  xrminltinf 10880 
Two ways of saying an extended real is greater than the minimum of two
others. (Contributed by Jim Kingdon, 19May2023.)

inf


Theorem  xrminrecl 10881 
The minimum of two real numbers is the same when taken as extended reals
or as reals. (Contributed by Jim Kingdon, 18May2023.)

inf inf 

Theorem  xrminrpcl 10882 
The minimum of two positive reals is a positive real. (Contributed by Jim
Kingdon, 4May2023.)

inf 

Theorem  xrminadd 10883 
Distributing addition over minimum. (Contributed by Jim Kingdon,
10May2023.)

inf inf 

Theorem  xrbdtri 10884 
Triangle inequality for bounded values. (Contributed by Jim Kingdon,
15May2023.)

inf
inf inf


Theorem  iooinsup 10885 
Intersection of two open intervals of extended reals. (Contributed by
NM, 7Feb2007.) (Revised by Jim Kingdon, 22May2023.)

inf 

3.8 Elementary limits and
convergence


3.8.1 Limits


Syntax  cli 10886 
Extend class notation with convergence relation for limits.



Definition  dfclim 10887* 
Define the limit relation for complex number sequences. See clim 10889
for
its relational expression. (Contributed by NM, 28Aug2005.)



Theorem  climrel 10888 
The limit relation is a relation. (Contributed by NM, 28Aug2005.)
(Revised by Mario Carneiro, 31Jan2014.)



Theorem  clim 10889* 
Express the predicate: The limit of complex number sequence is
, or converges to . This means that for any
real
, no matter how
small, there always exists an integer such
that the absolute difference of any later complex number in the sequence
and the limit is less than . (Contributed by NM, 28Aug2005.)
(Revised by Mario Carneiro, 28Apr2015.)



Theorem  climcl 10890 
Closure of the limit of a sequence of complex numbers. (Contributed by
NM, 28Aug2005.) (Revised by Mario Carneiro, 28Apr2015.)



Theorem  clim2 10891* 
Express the predicate: The limit of complex number sequence is
, or converges to , with more general
quantifier
restrictions than clim 10889. (Contributed by NM, 6Jan2007.) (Revised
by Mario Carneiro, 31Jan2014.)



Theorem  clim2c 10892* 
Express the predicate
converges to .
(Contributed by NM,
24Feb2008.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  clim0 10893* 
Express the predicate
converges to .
(Contributed by NM,
24Feb2008.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  clim0c 10894* 
Express the predicate
converges to .
(Contributed by NM,
24Feb2008.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climi 10895* 
Convergence of a sequence of complex numbers. (Contributed by NM,
11Jan2007.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climi2 10896* 
Convergence of a sequence of complex numbers. (Contributed by NM,
11Jan2007.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climi0 10897* 
Convergence of a sequence of complex numbers to zero. (Contributed by
NM, 11Jan2007.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climconst 10898* 
An (eventually) constant sequence converges to its value. (Contributed
by NM, 28Aug2005.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climconst2 10899 
A constant sequence converges to its value. (Contributed by NM,
6Feb2008.) (Revised by Mario Carneiro, 31Jan2014.)



Theorem  climz 10900 
The zero sequence converges to zero. (Contributed by NM, 2Oct1999.)
(Revised by Mario Carneiro, 31Jan2014.)

