Theorem List for Intuitionistic Logic Explorer - 9701-9800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | abs3dif 9701 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
|
|
Theorem | abs2dif 9702 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
|
|
Theorem | abs2dif2 9703 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
|
|
Theorem | abs2difabs 9704 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
|
|
Theorem | recan 9705* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
|
|
Theorem | absf 9706 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
|
|
Theorem | abs3lem 9707 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | fzomaxdiflem 9708 |
Lemma for fzomaxdif 9709. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^ ..^ ..^ |
|
Theorem | fzomaxdif 9709 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^
..^ ..^ |
|
Theorem | cau3lem 9710* |
Lemma for cau3 9711. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
|
|
Theorem | cau3 9711* |
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 9587
and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.)
|
|
|
Theorem | cau4 9712* |
Change the base of a Cauchy criterion. (Contributed by Mario
Carneiro, 18-Mar-2014.)
|
|
|
Theorem | caubnd2 9713* |
A Cauchy sequence of complex numbers is eventually bounded.
(Contributed by Mario Carneiro, 14-Feb-2014.)
|
|
|
Theorem | amgm2 9714 |
Arithmetic-geometric mean inequality for
. (Contributed by
Mario Carneiro, 2-Jul-2014.)
|
|
|
Theorem | sqrtthi 9715 |
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 9716 |
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 9717 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtmsqi 9718 |
Square root of square. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | sqrtsqi 9719 |
Square root of square. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | sqsqrti 9720 |
Square of square root. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | sqrtge0i 9721 |
The square root of a nonnegative real is nonnegative. (Contributed by
NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | absidi 9722 |
A nonnegative number is its own absolute value. (Contributed by NM,
2-Aug-1999.)
|
|
|
Theorem | absnidi 9723 |
A negative number is the negative of its own absolute value.
(Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | leabsi 9724 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 2-Aug-1999.)
|
|
|
Theorem | absrei 9725 |
Absolute value of a real number. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrtpclii 9726 |
The square root of a positive real is a real. (Contributed by Mario
Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrtgt0ii 9727 |
The square root of a positive real is positive. (Contributed by NM,
26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.)
|
|
|
Theorem | sqrt11i 9728 |
The square root function is one-to-one. (Contributed by NM,
27-Jul-1999.)
|
|
|
Theorem | sqrtmuli 9729 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
|
|
Theorem | sqrtmulii 9730 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.)
|
|
|
Theorem | sqrtmsq2i 9731 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.)
|
|
|
Theorem | sqrtlei 9732 |
Square root is monotonic. (Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | sqrtlti 9733 |
Square root is strictly monotonic. (Contributed by Roy F. Longton,
8-Aug-2005.)
|
|
|
Theorem | abslti 9734 |
Absolute value and 'less than' relation. (Contributed by NM,
6-Apr-2005.)
|
|
|
Theorem | abslei 9735 |
Absolute value and 'less than or equal to' relation. (Contributed by
NM, 6-Apr-2005.)
|
|
|
Theorem | absvalsqi 9736 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | absvalsq2i 9737 |
Square of value of absolute value function. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | abscli 9738 |
Real closure of absolute value. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | absge0i 9739 |
Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | absval2i 9740 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 2-Oct-1999.)
|
|
|
Theorem | abs00i 9741 |
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 9742 |
The absolute value of a nonzero number is positive. Remark in [Apostol]
p. 363. (Contributed by NM, 1-Oct-1999.)
|
# |
|
Theorem | absnegi 9743 |
Absolute value of negative. (Contributed by NM, 2-Aug-1999.)
|
|
|
Theorem | abscji 9744 |
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 9745 |
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 9746 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by NM, 1-Oct-1999.)
|
|
|
Theorem | absmuli 9747 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
NM, 1-Oct-1999.)
|
|
|
Theorem | sqabsaddi 9748 |
Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason]
p. 133. (Contributed by NM, 2-Oct-1999.)
|
|
|
Theorem | sqabssubi 9749 |
Square of absolute value of difference. (Contributed by Steve
Rodriguez, 20-Jan-2007.)
|
|
|
Theorem | absdivapzi 9750 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
13-Aug-2021.)
|
# |
|
Theorem | abstrii 9751 |
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 9752 |
Absolute value of differences around common element. (Contributed by
NM, 2-Oct-1999.)
|
|
|
Theorem | abs3lemi 9753 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
|
|
Theorem | rpsqrtcld 9754 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtgt0d 9755 |
The square root of a positive real is positive. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absnidd 9756 |
A negative number is the negative of its own absolute value.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | leabsd 9757 |
A real number is less than or equal to its absolute value. (Contributed
by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absred 9758 |
Absolute value of a real number. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | resqrtcld 9759 |
The square root of a nonnegative real is a real. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmsqd 9760 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsqd 9761 |
Square root of square. (Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtge0d 9762 |
The square root of a nonnegative real is nonnegative. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absidd 9763 |
A nonnegative number is its own absolute value. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtdivd 9764 |
Square root distributes over division. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtmuld 9765 |
Square root distributes over multiplication. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtsq2d 9766 |
Relationship between square root and squares. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | sqrtled 9767 |
Square root is monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | sqrtltd 9768 |
Square root is strictly monotonic. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | sqr11d 9769 |
The square root function is one-to-one. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absltd 9770 |
Absolute value and 'less than' relation. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absled 9771 |
Absolute value and 'less than or equal to' relation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubge0d 9772 |
Absolute value of a nonnegative difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abssuble0d 9773 |
Absolute value of a nonpositive difference. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absdifltd 9774 |
The absolute value of a difference and 'less than' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absdifled 9775 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | icodiamlt 9776 |
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 9777 |
Real closure of absolute value. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absvalsqd 9778 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absvalsq2d 9779 |
Square of value of absolute value function. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | absge0d 9780 |
Absolute value is nonnegative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absval2d 9781 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs00d 9782 |
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 9783 |
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 9784 |
The absolute value of a complex number apart from zero is a positive
real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|
# |
|
Theorem | absnegd 9785 |
Absolute value of negative. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abscjd 9786 |
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 9787 |
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 9788 |
Absolute value of positive integer exponentiation. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abssubd 9789 |
Swapping order of subtraction doesn't change the absolute value.
Example of [Apostol] p. 363.
(Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | absmuld 9790 |
Absolute value distributes over multiplication. Proposition 10-3.7(f)
of [Gleason] p. 133. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | absdivapd 9791 |
Absolute value distributes over division. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
#
|
|
Theorem | abstrid 9792 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abs2difd 9793 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abs2dif2d 9794 |
Difference of absolute values. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | abs2difabsd 9795 |
Absolute value of difference of absolute values. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | abs3difd 9796 |
Absolute value of differences around common element. (Contributed by
Mario Carneiro, 29-May-2016.)
|
|
|
Theorem | abs3lemd 9797 |
Lemma involving absolute value of differences. (Contributed by Mario
Carneiro, 29-May-2016.)
|
|
|
Theorem | qdenre 9798* |
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 9111. (Contributed by BJ, 15-Oct-2021.)
|
|
|
3.8 Elementary limits and
convergence
|
|
3.8.1 Limits
|
|
Syntax | cli 9799 |
Extend class notation with convergence relation for limits.
|
|
|
Definition | df-clim 9800* |
Define the limit relation for complex number sequences. See clim 9802
for
its relational expression. (Contributed by NM, 28-Aug-2005.)
|
|