Theorem List for Intuitionistic Logic Explorer - 9901-10000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | resqrexlemcalc2 9901* |
Lemma for resqrex 9912. Some of the calculations involved in
showing
that the sequence converges. (Contributed by Mario Carneiro and Jim
Kingdon, 29-Jul-2021.)
|
|
|
Theorem | resqrexlemcalc3 9902* |
Lemma for resqrex 9912. Some of the calculations involved in
showing
that the sequence converges. (Contributed by Mario Carneiro and Jim
Kingdon, 29-Jul-2021.)
|
|
|
Theorem | resqrexlemnmsq 9903* |
Lemma for resqrex 9912. The difference between the squares of two
terms
of the sequence. (Contributed by Mario Carneiro and Jim Kingdon,
30-Jul-2021.)
|
|
|
Theorem | resqrexlemnm 9904* |
Lemma for resqrex 9912. The difference between two terms of the
sequence. (Contributed by Mario Carneiro and Jim Kingdon,
31-Jul-2021.)
|
|
|
Theorem | resqrexlemcvg 9905* |
Lemma for resqrex 9912. The sequence has a limit. (Contributed by
Jim
Kingdon, 6-Aug-2021.)
|
|
|
Theorem | resqrexlemgt0 9906* |
Lemma for resqrex 9912. A limit is nonnegative. (Contributed by
Jim
Kingdon, 7-Aug-2021.)
|
|
|
Theorem | resqrexlemoverl 9907* |
Lemma for resqrex 9912. Every term in the sequence is an
overestimate
compared with the limit . Although this theorem is stated in
terms of a particular sequence the proof could be adapted for any
decreasing convergent sequence. (Contributed by Jim Kingdon,
9-Aug-2021.)
|
|
|
Theorem | resqrexlemglsq 9908* |
Lemma for resqrex 9912. The sequence formed by squaring each term
of
converges to .
(Contributed by Mario
Carneiro and Jim Kingdon, 8-Aug-2021.)
|
|
|
Theorem | resqrexlemga 9909* |
Lemma for resqrex 9912. The sequence formed by squaring each term
of
converges to .
(Contributed by Mario Carneiro and
Jim Kingdon, 8-Aug-2021.)
|
|
|
Theorem | resqrexlemsqa 9910* |
Lemma for resqrex 9912. The square of a limit is .
(Contributed by Jim Kingdon, 7-Aug-2021.)
|
|
|
Theorem | resqrexlemex 9911* |
Lemma for resqrex 9912. Existence of square root given a sequence
which
converges to the square root. (Contributed by Mario Carneiro and Jim
Kingdon, 27-Jul-2021.)
|
|
|
Theorem | resqrex 9912* |
Existence of a square root for positive reals. (Contributed by Mario
Carneiro, 9-Jul-2013.)
|
|
|
Theorem | rsqrmo 9913* |
Uniqueness for the square root function. (Contributed by Jim Kingdon,
10-Aug-2021.)
|
|
|
Theorem | rersqreu 9914* |
Existence and uniqueness for the real square root function.
(Contributed by Jim Kingdon, 10-Aug-2021.)
|
|
|
Theorem | resqrtcl 9915 |
Closure of the square root function. (Contributed by Mario Carneiro,
9-Jul-2013.)
|
|
|
Theorem | rersqrtthlem 9916 |
Lemma for resqrtth 9917. (Contributed by Jim Kingdon, 10-Aug-2021.)
|
|
|
Theorem | resqrtth 9917 |
Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29.
(Contributed by Mario Carneiro, 9-Jul-2013.)
|
|
|
Theorem | remsqsqrt 9918 |
Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|
|
|
Theorem | sqrtge0 9919 |
The square root function is nonnegative for nonnegative input.
(Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro,
9-Jul-2013.)
|
|
|
Theorem | sqrtgt0 9920 |
The square root function is positive for positive input. (Contributed by
Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtmul 9921 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtle 9922 |
Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof
shortened by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtlt 9923 |
Square root is strictly monotonic. Closed form of sqrtlti 10023.
(Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrt11ap 9924 |
Analogue to sqrt11 9925 but for apartness. (Contributed by Jim
Kingdon,
11-Aug-2021.)
|
# # |
|
Theorem | sqrt11 9925 |
The square root function is one-to-one. Also see sqrt11ap 9924 which would
follow easily from this given excluded middle, but which is proved another
way without it. (Contributed by Scott Fenton, 11-Jun-2013.)
|
|
|
Theorem | sqrt00 9926 |
A square root is zero iff its argument is 0. (Contributed by NM,
27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | rpsqrtcl 9927 |
The square root of a positive real is a positive real. (Contributed by
NM, 22-Feb-2008.)
|
|
|
Theorem | sqrtdiv 9928 |
Square root distributes over division. (Contributed by Mario Carneiro,
5-May-2016.)
|
|
|
Theorem | sqrtsq2 9929 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsq 9930 |
Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmsq 9931 |
Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrt1 9932 |
The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|
|
|
Theorem | sqrt4 9933 |
The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrt9 9934 |
The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | sqrt2gt1lt2 9935 |
The square root of 2 is bounded by 1 and 2. (Contributed by Roy F.
Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | absneg 9936 |
Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|
|
|
Theorem | abscl 9937 |
Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|
|
|
Theorem | abscj 9938 |
The absolute value of a number and its conjugate are the same.
Proposition 10-3.7(b) of [Gleason] p. 133.
(Contributed by NM,
28-Apr-2005.)
|
|
|
Theorem | absvalsq 9939 |
Square of value of absolute value function. (Contributed by NM,
16-Jan-2006.)
|
|
|
Theorem | absvalsq2 9940 |
Square of value of absolute value function. (Contributed by NM,
1-Feb-2007.)
|
|
|
Theorem | sqabsadd 9941 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 21-Jan-2007.)
|
|
|
Theorem | sqabssub 9942 |
Square of absolute value of difference. (Contributed by NM,
21-Jan-2007.)
|
|
|
Theorem | absval2 9943 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 17-Mar-2005.)
|
|
|
Theorem | abs0 9944 |
The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absi 9945 |
The absolute value of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
|
|
Theorem | absge0 9946 |
Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.)
(Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absrpclap 9947 |
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
#
|
|
Theorem | abs00ap 9948 |
The absolute value of a number is apart from zero iff the number is apart
from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|
#
#
|
|
Theorem | absext 9949 |
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
# # |
|
Theorem | abs00 9950 |
The absolute value of a number is zero iff the number is zero. Also see
abs00ap 9948 which is similar but for apartness.
Proposition 10-3.7(c) of
[Gleason] p. 133. (Contributed by NM,
26-Sep-2005.) (Proof shortened by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs00ad 9951 |
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 9950. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | abs00bd 9952 |
If a complex number is zero, its absolute value is zero. (Contributed
by David Moews, 28-Feb-2017.)
|
|
|
Theorem | absreimsq 9953 |
Square of the absolute value of a number that has been decomposed into
real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
|
|
|
Theorem | absreim 9954 |
Absolute value of a number that has been decomposed into real and
imaginary parts. (Contributed by NM, 14-Jan-2006.)
|
|
|
Theorem | absmul 9955 |
Absolute value distributes over multiplication. Proposition 10-3.7(f) of
[Gleason] p. 133. (Contributed by NM,
11-Oct-1999.) (Revised by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absdivap 9956 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
# |
|
Theorem | absid 9957 |
A nonnegative number is its own absolute value. (Contributed by NM,
11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs1 9958 |
The absolute value of 1. Common special case. (Contributed by David A.
Wheeler, 16-Jul-2016.)
|
|
|
Theorem | absnid 9959 |
A negative number is the negative of its own absolute value. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | leabs 9960 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | qabsor 9961 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
|
|
Theorem | qabsord 9962 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
|
|
Theorem | absre 9963 |
Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|
|
|
Theorem | absresq 9964 |
Square of the absolute value of a real number. (Contributed by NM,
16-Jan-2006.)
|
|
|
Theorem | absexp 9965 |
Absolute value of positive integer exponentiation. (Contributed by NM,
5-Jan-2006.)
|
|
|
Theorem | absexpzap 9966 |
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
#
|
|
Theorem | abssq 9967 |
Square can be moved in and out of absolute value. (Contributed by Scott
Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | sqabs 9968 |
The squares of two reals are equal iff their absolute values are equal.
(Contributed by NM, 6-Mar-2009.)
|
|
|
Theorem | absrele 9969 |
The absolute value of a complex number is greater than or equal to the
absolute value of its real part. (Contributed by NM, 1-Apr-2005.)
|
|
|
Theorem | absimle 9970 |
The absolute value of a complex number is greater than or equal to the
absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.)
(Proof shortened by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | nn0abscl 9971 |
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | zabscl 9972 |
The absolute value of an integer is an integer. (Contributed by Stefan
O'Rear, 24-Sep-2014.)
|
|
|
Theorem | ltabs 9973 |
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12-Aug-2021.)
|
|
|
Theorem | abslt 9974 |
Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
(Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absle 9975 |
Absolute value and 'less than or equal to' relation. (Contributed by NM,
6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubap0 9976 |
If the absolute value of a complex number is less than a real, its
difference from the real is apart from zero. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
# |
|
Theorem | abssubne0 9977 |
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 9976 which is the
same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|
|
|
Theorem | absdiflt 9978 |
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18-Sep-2007.)
|
|
|
Theorem | absdifle 9979 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18-Sep-2007.)
|
|
|
Theorem | elicc4abs 9980 |
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16-Nov-2014.)
|
|
|
Theorem | lenegsq 9981 |
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16-Jan-2006.)
|
|
|
Theorem | releabs 9982 |
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,
1-Apr-2005.)
|
|
|
Theorem | recvalap 9983 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
#
|
|
Theorem | absidm 9984 |
The absolute value function is idempotent. (Contributed by NM,
20-Nov-2004.)
|
|
|
Theorem | absgt0ap 9985 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
# |
|
Theorem | nnabscl 9986 |
The absolute value of a nonzero integer is a positive integer.
(Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew
Salmon, 25-May-2011.)
|
|
|
Theorem | abssub 9987 |
Swapping order of subtraction doesn't change the absolute value.
(Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abssubge0 9988 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
|
|
Theorem | abssuble0 9989 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
|
|
Theorem | abstri 9990 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by NM,
7-Mar-2005.) (Proof shortened by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs3dif 9991 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
|
|
Theorem | abs2dif 9992 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
|
|
Theorem | abs2dif2 9993 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
|
|
Theorem | abs2difabs 9994 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
|
|
Theorem | recan 9995* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
|
|
Theorem | absf 9996 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
|
|
Theorem | abs3lem 9997 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | fzomaxdiflem 9998 |
Lemma for fzomaxdif 9999. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^ ..^ ..^ |
|
Theorem | fzomaxdif 9999 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^
..^ ..^ |
|
Theorem | cau3lem 10000* |
Lemma for cau3 10001. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
|