Theorem List for Intuitionistic Logic Explorer - 10801-10900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | sqrtle 10801 |
Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof
shortened by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtlt 10802 |
Square root is strictly monotonic. Closed form of sqrtlti 10902.
(Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrt11ap 10803 |
Analogue to sqrt11 10804 but for apartness. (Contributed by Jim
Kingdon,
11-Aug-2021.)
|
# # |
|
Theorem | sqrt11 10804 |
The square root function is one-to-one. Also see sqrt11ap 10803 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 10805 |
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 10806 |
The square root of a positive real is a positive real. (Contributed by
NM, 22-Feb-2008.)
|
|
|
Theorem | sqrtdiv 10807 |
Square root distributes over division. (Contributed by Mario Carneiro,
5-May-2016.)
|
|
|
Theorem | sqrtsq2 10808 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsq 10809 |
Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmsq 10810 |
Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrt1 10811 |
The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|
|
|
Theorem | sqrt4 10812 |
The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrt9 10813 |
The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|
|
|
Theorem | sqrt2gt1lt2 10814 |
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 10815 |
Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|
|
|
Theorem | abscl 10816 |
Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|
|
|
Theorem | abscj 10817 |
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 10818 |
Square of value of absolute value function. (Contributed by NM,
16-Jan-2006.)
|
|
|
Theorem | absvalsq2 10819 |
Square of value of absolute value function. (Contributed by NM,
1-Feb-2007.)
|
|
|
Theorem | sqabsadd 10820 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 21-Jan-2007.)
|
|
|
Theorem | sqabssub 10821 |
Square of absolute value of difference. (Contributed by NM,
21-Jan-2007.)
|
|
|
Theorem | absval2 10822 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 17-Mar-2005.)
|
|
|
Theorem | abs0 10823 |
The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absi 10824 |
The absolute value of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
|
|
Theorem | absge0 10825 |
Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.)
(Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absrpclap 10826 |
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
#
|
|
Theorem | abs00ap 10827 |
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 10828 |
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
# # |
|
Theorem | abs00 10829 |
The absolute value of a number is zero iff the number is zero. Also see
abs00ap 10827 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 10830 |
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 10829. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | abs00bd 10831 |
If a complex number is zero, its absolute value is zero. (Contributed
by David Moews, 28-Feb-2017.)
|
|
|
Theorem | absreimsq 10832 |
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 10833 |
Absolute value of a number that has been decomposed into real and
imaginary parts. (Contributed by NM, 14-Jan-2006.)
|
|
|
Theorem | absmul 10834 |
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 10835 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
# |
|
Theorem | absid 10836 |
A nonnegative number is its own absolute value. (Contributed by NM,
11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs1 10837 |
The absolute value of 1. Common special case. (Contributed by David A.
Wheeler, 16-Jul-2016.)
|
|
|
Theorem | absnid 10838 |
A negative number is the negative of its own absolute value. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | leabs 10839 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | qabsor 10840 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
|
|
Theorem | qabsord 10841 |
The absolute value of a rational number is either that number or its
negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
|
|
|
Theorem | absre 10842 |
Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|
|
|
Theorem | absresq 10843 |
Square of the absolute value of a real number. (Contributed by NM,
16-Jan-2006.)
|
|
|
Theorem | absexp 10844 |
Absolute value of positive integer exponentiation. (Contributed by NM,
5-Jan-2006.)
|
|
|
Theorem | absexpzap 10845 |
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
#
|
|
Theorem | abssq 10846 |
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 10847 |
The squares of two reals are equal iff their absolute values are equal.
(Contributed by NM, 6-Mar-2009.)
|
|
|
Theorem | absrele 10848 |
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 10849 |
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 10850 |
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27-Feb-2005.)
|
|
|
Theorem | zabscl 10851 |
The absolute value of an integer is an integer. (Contributed by Stefan
O'Rear, 24-Sep-2014.)
|
|
|
Theorem | ltabs 10852 |
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12-Aug-2021.)
|
|
|
Theorem | abslt 10853 |
Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
(Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absle 10854 |
Absolute value and 'less than or equal to' relation. (Contributed by NM,
6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubap0 10855 |
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 10856 |
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 10855 which is the
same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|
|
|
Theorem | absdiflt 10857 |
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18-Sep-2007.)
|
|
|
Theorem | absdifle 10858 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18-Sep-2007.)
|
|
|
Theorem | elicc4abs 10859 |
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16-Nov-2014.)
|
|
|
Theorem | lenegsq 10860 |
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16-Jan-2006.)
|
|
|
Theorem | releabs 10861 |
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 10862 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
#
|
|
Theorem | absidm 10863 |
The absolute value function is idempotent. (Contributed by NM,
20-Nov-2004.)
|
|
|
Theorem | absgt0ap 10864 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
# |
|
Theorem | nnabscl 10865 |
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 10866 |
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 10867 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
|
|
Theorem | abssuble0 10868 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
|
|
Theorem | abstri 10869 |
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 10870 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
|
|
Theorem | abs2dif 10871 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
|
|
Theorem | abs2dif2 10872 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
|
|
Theorem | abs2difabs 10873 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
|
|
Theorem | recan 10874* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
|
|
Theorem | absf 10875 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
|
|
Theorem | abs3lem 10876 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | fzomaxdiflem 10877 |
Lemma for fzomaxdif 10878. (Contributed by Stefan O'Rear,
6-Sep-2015.)
|
..^ ..^ ..^ |
|
Theorem | fzomaxdif 10878 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^
..^ ..^ |
|
Theorem | cau3lem 10879* |
Lemma for cau3 10880. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | cau3 10880* |
Convert between three-quantifier and four-quantifier versions of the
Cauchy criterion. (In particular, the four-quantifier version has no
occurrence of in
the assertion, so it can be used with rexanuz 10753
and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|
|
|
Theorem | cau4 10881* |
Change the base of a Cauchy criterion. (Contributed by Mario
Carneiro, 18-Mar-2014.)
|
|
|
Theorem | caubnd2 10882* |
A Cauchy sequence of complex numbers is eventually bounded.
(Contributed by Mario Carneiro, 14-Feb-2014.)
|
|
|
Theorem | amgm2 10883 |
Arithmetic-geometric mean inequality for
. (Contributed by
Mario Carneiro, 2-Jul-2014.)
|
|
|
Theorem | sqrtthi 10884 |
Square root theorem. Theorem I.35 of [Apostol]
p. 29. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtcli 10885 |
The square root of a nonnegative real is a real. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtgt0i 10886 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtmsqi 10887 |
Square root of square. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqrtsqi 10888 |
Square root of square. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | sqsqrti 10889 |
Square of square root. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | sqrtge0i 10890 |
The square root of a nonnegative real is nonnegative. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | absidi 10891 |
A nonnegative number is its own absolute value. (Contributed by NM,
2-Aug-1999.)
|
|
|
Theorem | absnidi 10892 |
A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | leabsi 10893 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 2-Aug-1999.)
|
|
|
Theorem | absrei 10894 |
Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrtpclii 10895 |
The square root of a positive real is a real. (Contributed by Mario
Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtgt0ii 10896 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrt11i 10897 |
The square root function is one-to-one. (Contributed by NM,
27-Jul-1999.)
|
|
|
Theorem | sqrtmuli 10898 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
|
|
Theorem | sqrtmulii 10899 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
|
|
Theorem | sqrtmsq2i 10900 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.)
|
|