Theorem List for Intuitionistic Logic Explorer - 10901-11000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sqrtlei 10901 |
Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrtlti 10902 |
Square root is strictly monotonic. (Contributed by Roy F. Longton,
8-Aug-2005.)
|
|
|
Theorem | abslti 10903 |
Absolute value and 'less than' relation. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | abslei 10904 |
Absolute value and 'less than or equal to' relation. (Contributed by
NM, 6-Apr-2005.)
|
|
|
Theorem | absvalsqi 10905 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | absvalsq2i 10906 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | abscli 10907 |
Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | absge0i 10908 |
Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | absval2i 10909 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
|
|
Theorem | abs00i 10910 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by NM,
28-Jul-1999.)
|
|
|
Theorem | absgt0api 10911 |
The absolute value of a nonzero number is positive. Remark in [Apostol]
p. 363. (Contributed by NM, 1-Oct-1999.)
|
# |
|
Theorem | absnegi 10912 |
Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | abscji 10913 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p.
133. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | releabsi 10914 |
The real part of a number is less than or equal to its absolute value.
Proposition 10-3.7(d) of [Gleason] p.
133. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | abssubi 10915 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by NM, 1-Oct-1999.)
|
|
|
Theorem | absmuli 10916 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
NM, 1-Oct-1999.)
|
|
|
Theorem | sqabsaddi 10917 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 2-Oct-1999.)
|
|
|
Theorem | sqabssubi 10918 |
Square of absolute value of difference. (Contributed by Steve
Rodriguez, 20-Jan-2007.)
|
|
|
Theorem | absdivapzi 10919 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
# |
|
Theorem | abstrii 10920 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. This is Metamath 100
proof #91. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | abs3difi 10921 |
Absolute value of differences around common element. (Contributed by
NM, 2-Oct-1999.)
|
|
|
Theorem | abs3lemi 10922 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | rpsqrtcld 10923 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtgt0d 10924 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absnidd 10925 |
A negative number is the negative of its own absolute value.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | leabsd 10926 |
A real number is less than or equal to its absolute value. (Contributed
by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absred 10927 |
Absolute value of a real number. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | resqrtcld 10928 |
The square root of a nonnegative real is a real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmsqd 10929 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsqd 10930 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtge0d 10931 |
The square root of a nonnegative real is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absidd 10932 |
A nonnegative number is its own absolute value. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtdivd 10933 |
Square root distributes over division. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmuld 10934 |
Square root distributes over multiplication. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsq2d 10935 |
Relationship between square root and squares. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtled 10936 |
Square root is monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | sqrtltd 10937 |
Square root is strictly monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | sqr11d 10938 |
The square root function is one-to-one. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absltd 10939 |
Absolute value and 'less than' relation. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absled 10940 |
Absolute value and 'less than or equal to' relation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubge0d 10941 |
Absolute value of a nonnegative difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abssuble0d 10942 |
Absolute value of a nonpositive difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absdifltd 10943 |
The absolute value of a difference and 'less than' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absdifled 10944 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | icodiamlt 10945 |
Two elements in a half-open interval have separation strictly less than
the difference between the endpoints. (Contributed by Stefan O'Rear,
12-Sep-2014.)
|
|
|
Theorem | abscld 10946 |
Real closure of absolute value. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absvalsqd 10947 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absvalsq2d 10948 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absge0d 10949 |
Absolute value is nonnegative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absval2d 10950 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs00d 10951 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absne0d 10952 |
The absolute value of a number is zero iff the number is zero.
Proposition 10-3.7(c) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absrpclapd 10953 |
The absolute value of a complex number apart from zero is a positive
real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|
# |
|
Theorem | absnegd 10954 |
Absolute value of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abscjd 10955 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | releabsd 10956 |
The real part of a number is less than or equal to its absolute value.
Proposition 10-3.7(d) of [Gleason] p.
133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absexpd 10957 |
Absolute value of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubd 10958 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absmuld 10959 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absdivapd 10960 |
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
#
|
|
Theorem | abstrid 10961 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abs2difd 10962 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abs2dif2d 10963 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abs2difabsd 10964 |
Absolute value of difference of absolute values. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abs3difd 10965 |
Absolute value of differences around common element. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs3lemd 10966 |
Lemma involving absolute value of differences. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | qdenre 10967* |
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 10027. (Contributed by BJ, 15-Oct-2021.)
|
|
|
4.7.5 The maximum of two real
numbers
|
|
Theorem | maxcom 10968 |
The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10.
(Contributed by Jim Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxabsle 10969 |
An upper bound for . (Contributed by Jim Kingdon,
20-Dec-2021.)
|
|
|
Theorem | maxleim 10970 |
Value of maximum when we know which number is larger. (Contributed by
Jim Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxabslemab 10971 |
Lemma for maxabs 10974. A variation of maxleim 10970- that is, if we know
which of two real numbers is larger, we know the maximum of the two.
(Contributed by Jim Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxabslemlub 10972 |
Lemma for maxabs 10974. A least upper bound for .
(Contributed by Jim Kingdon, 20-Dec-2021.)
|
|
|
Theorem | maxabslemval 10973* |
Lemma for maxabs 10974. Value of the supremum. (Contributed by
Jim
Kingdon, 22-Dec-2021.)
|
|
|
Theorem | maxabs 10974 |
Maximum of two real numbers in terms of absolute value. (Contributed by
Jim Kingdon, 20-Dec-2021.)
|
|
|
Theorem | maxcl 10975 |
The maximum of two real numbers is a real number. (Contributed by Jim
Kingdon, 22-Dec-2021.)
|
|
|
Theorem | maxle1 10976 |
The maximum of two reals is no smaller than the first real. Lemma 3.10 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxle2 10977 |
The maximum of two reals is no smaller than the second real. Lemma 3.10
of [Geuvers], p. 10. (Contributed by Jim
Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxleast 10978 |
The maximum of two reals is a least upper bound. Lemma 3.11 of
[Geuvers], p. 10. (Contributed by Jim
Kingdon, 22-Dec-2021.)
|
|
|
Theorem | maxleastb 10979 |
Two ways of saying the maximum of two numbers is less than or equal to a
third. (Contributed by Jim Kingdon, 31-Jan-2022.)
|
|
|
Theorem | maxleastlt 10980 |
The maximum as a least upper bound, in terms of less than. (Contributed
by Jim Kingdon, 9-Feb-2022.)
|
|
|
Theorem | maxleb 10981 |
Equivalence of
and being equal to the maximum of two reals. Lemma
3.12 of [Geuvers], p. 10. (Contributed by
Jim Kingdon, 21-Dec-2021.)
|
|
|
Theorem | dfabsmax 10982 |
Absolute value of a real number in terms of maximum. Definition 3.13 of
[Geuvers], p. 11. (Contributed by BJ and
Jim Kingdon, 21-Dec-2021.)
|
|
|
Theorem | maxltsup 10983 |
Two ways of saying the maximum of two numbers is less than a third.
(Contributed by Jim Kingdon, 10-Feb-2022.)
|
|
|
Theorem | max0addsup 10984 |
The sum of the positive and negative part functions is the absolute value
function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
|
|
|
Theorem | rexanre 10985* |
Combine two different upper real properties into one. (Contributed by
Mario Carneiro, 8-May-2016.)
|
|
|
Theorem | rexico 10986* |
Restrict the base of an upper real quantifier to an upper real set.
(Contributed by Mario Carneiro, 12-May-2016.)
|
|
|
Theorem | maxclpr 10987 |
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 9091 if one is dealing with integers, but real
number
dichotomy in general does not follow from our axioms. (Contributed by Jim
Kingdon, 1-Feb-2022.)
|
|
|
Theorem | rpmaxcl 10988 |
The maximum of two positive real numbers is a positive real number.
(Contributed by Jim Kingdon, 10-Nov-2023.)
|
|
|
Theorem | zmaxcl 10989 |
The maximum of two integers is an integer. (Contributed by Jim Kingdon,
27-Sep-2022.)
|
|
|
Theorem | 2zsupmax 10990 |
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, 22-Jan-2023.)
|
|
|
Theorem | fimaxre2 10991* |
A nonempty finite set of real numbers has an upper bound. (Contributed
by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro,
13-Feb-2014.)
|
|
|
Theorem | negfi 10992* |
The negation of a finite set of real numbers is finite. (Contributed by
AV, 9-Aug-2020.)
|
|
|
4.7.6 The minimum of two real
numbers
|
|
Theorem | mincom 10993 |
The minimum of two reals is commutative. (Contributed by Jim Kingdon,
8-Feb-2021.)
|
inf inf
|
|
Theorem | minmax 10994 |
Minimum expressed in terms of maximum. (Contributed by Jim Kingdon,
8-Feb-2021.)
|
inf |
|
Theorem | mincl 10995 |
The minumum of two real numbers is a real number. (Contributed by Jim
Kingdon, 25-Apr-2023.)
|
inf |
|
Theorem | min1inf 10996 |
The minimum of two numbers is less than or equal to the first.
(Contributed by Jim Kingdon, 8-Feb-2021.)
|
inf |
|
Theorem | min2inf 10997 |
The minimum of two numbers is less than or equal to the second.
(Contributed by Jim Kingdon, 9-Feb-2021.)
|
inf |
|
Theorem | lemininf 10998 |
Two ways of saying a number is less than or equal to the minimum of two
others. (Contributed by NM, 3-Aug-2007.)
|
inf
|
|
Theorem | ltmininf 10999 |
Two ways of saying a number is less than the minimum of two others.
(Contributed by Jim Kingdon, 10-Feb-2022.)
|
inf |
|
Theorem | minabs 11000 |
The minimum of two real numbers in terms of absolute value. (Contributed
by Jim Kingdon, 15-May-2023.)
|
inf
|