Home | Intuitionistic Logic Explorer Theorem List (p. 108 of 132) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | redivapd 10701 | Real part of a division. Related to remul2 10600. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | imdivapd 10702 | Imaginary part of a division. Related to remul2 10600. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | crred 10703 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | crimd 10704 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cnreim 10705 | Complex apartness in terms of real and imaginary parts. See also apreim 8332 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
Theorem | caucvgrelemrec 10706* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
# | ||
Theorem | caucvgrelemcau 10707* | Lemma for caucvgre 10708. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
Theorem | caucvgre 10708* |
Convergence of real sequences.
A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.) |
Theorem | cvg1nlemcxze 10709 | Lemma for cvg1n 10713. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | cvg1nlemf 10710* | Lemma for cvg1n 10713. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemcau 10711* | Lemma for cvg1n 10713. By selecting spaced out terms for the modified sequence , the terms are within (without the constant ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemres 10712* | Lemma for cvg1n 10713. The original sequence has a limit (turns out it is the same as the limit of the modified sequence ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1n 10713* |
Convergence of real sequences.
This is a version of caucvgre 10708 with a constant multiplier on the rate of convergence. That is, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | uzin2 10714 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | rexanuz 10715* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
Theorem | rexfiuz 10716* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
Theorem | rexuz3 10717* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | rexanuz2 10718* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | r19.29uz 10719* | A version of 19.29 1584 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
Theorem | r19.2uz 10720* | A version of r19.2m 3419 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
Theorem | recvguniqlem 10721 | Lemma for recvguniq 10722. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Theorem | recvguniq 10722* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Syntax | csqrt 10723 | Extend class notation to include square root of a complex number. |
Syntax | cabs 10724 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-rsqrt 10725* |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Definition | df-abs 10726 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtrval 10727* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Theorem | absval 10728 | The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | rennim 10729 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | sqrt0rlem 10730 | Lemma for sqrt0 10731. (Contributed by Jim Kingdon, 26-Aug-2020.) |
Theorem | sqrt0 10731 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrexlem1arp 10732 | Lemma for resqrex 10753. is a positive real (expressed in a way that will help apply seqf 10189 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemp1rp 10733* | Lemma for resqrex 10753. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10189 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf 10734* | Lemma for resqrex 10753. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf1 10735* | Lemma for resqrex 10753. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemfp1 10736* | Lemma for resqrex 10753. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemover 10737* | Lemma for resqrex 10753. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemdec 10738* | Lemma for resqrex 10753. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemdecn 10739* | Lemma for resqrex 10753. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemlo 10740* | Lemma for resqrex 10753. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc1 10741* | Lemma for resqrex 10753. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc2 10742* | Lemma for resqrex 10753. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc3 10743* | Lemma for resqrex 10753. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemnmsq 10744* | Lemma for resqrex 10753. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
Theorem | resqrexlemnm 10745* | Lemma for resqrex 10753. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemcvg 10746* | Lemma for resqrex 10753. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | resqrexlemgt0 10747* | Lemma for resqrex 10753. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemoverl 10748* | Lemma for resqrex 10753. 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 10749* | Lemma for resqrex 10753. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemga 10750* | Lemma for resqrex 10753. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemsqa 10751* | Lemma for resqrex 10753. The square of a limit is . (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemex 10752* | Lemma for resqrex 10753. 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 10753* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | rsqrmo 10754* | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | rersqreu 10755* | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | resqrtcl 10756 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | rersqrtthlem 10757 | Lemma for resqrtth 10758. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | resqrtth 10758 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | remsqsqrt 10759 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrtge0 10760 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrtgt0 10761 | 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 10762 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtle 10763 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtlt 10764 | Square root is strictly monotonic. Closed form of sqrtlti 10864. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | sqrt11ap 10765 | Analogue to sqrt11 10766 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# # | ||
Theorem | sqrt11 10766 | The square root function is one-to-one. Also see sqrt11ap 10765 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 10767 | 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 10768 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
Theorem | sqrtdiv 10769 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
Theorem | sqrtsq2 10770 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtsq 10771 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtmsq 10772 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrt1 10773 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
Theorem | sqrt4 10774 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
Theorem | sqrt9 10775 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
Theorem | sqrt2gt1lt2 10776 | 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 10777 | Absolute value of negative. (Contributed by NM, 27-Feb-2005.) |
Theorem | abscl 10778 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
Theorem | abscj 10779 | 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 10780 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
Theorem | absvalsq2 10781 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
Theorem | sqabsadd 10782 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) |
Theorem | sqabssub 10783 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
Theorem | absval2 10784 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
Theorem | abs0 10785 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | absi 10786 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
Theorem | absge0 10787 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | absrpclap 10788 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# | ||
Theorem | abs00ap 10789 | 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 10790 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) |
# # | ||
Theorem | abs00 10791 | The absolute value of a number is zero iff the number is zero. Also see abs00ap 10789 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 10792 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 10791. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | abs00bd 10793 | If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | absreimsq 10794 | 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 10795 | Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.) |
Theorem | absmul 10796 | 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 10797 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# | ||
Theorem | absid 10798 | A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | abs1 10799 | The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.) |
Theorem | absnid 10800 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |