Home | Intuitionistic Logic Explorer Theorem List (p. 110 of 138) | < 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 | immul2d 10901 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | redivapd 10902 | Real part of a division. Related to remul2 10801. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | imdivapd 10903 | Imaginary part of a division. Related to remul2 10801. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | crred 10904 | 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 10905 | 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 10906 | Complex apartness in terms of real and imaginary parts. See also apreim 8492 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
Theorem | caucvgrelemrec 10907* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
# | ||
Theorem | caucvgrelemcau 10908* | Lemma for caucvgre 10909. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
Theorem | caucvgre 10909* |
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 10910 | Lemma for cvg1n 10914. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | cvg1nlemf 10911* | Lemma for cvg1n 10914. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemcau 10912* | Lemma for cvg1n 10914. 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 10913* | Lemma for cvg1n 10914. 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 10914* |
Convergence of real sequences.
This is a version of caucvgre 10909 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 10915 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | rexanuz 10916* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
Theorem | rexfiuz 10917* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
Theorem | rexuz3 10918* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | rexanuz2 10919* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | r19.29uz 10920* | A version of 19.29 1607 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
Theorem | r19.2uz 10921* | A version of r19.2m 3490 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
Theorem | recvguniqlem 10922 | Lemma for recvguniq 10923. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Theorem | recvguniq 10923* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Syntax | csqrt 10924 | Extend class notation to include square root of a complex number. |
Syntax | cabs 10925 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-rsqrt 10926* |
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 10927 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtrval 10928* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Theorem | absval 10929 | 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 10930 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | sqrt0rlem 10931 | Lemma for sqrt0 10932. (Contributed by Jim Kingdon, 26-Aug-2020.) |
Theorem | sqrt0 10932 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrexlem1arp 10933 | Lemma for resqrex 10954. is a positive real (expressed in a way that will help apply seqf 10386 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemp1rp 10934* | Lemma for resqrex 10954. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10386 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf 10935* | Lemma for resqrex 10954. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf1 10936* | Lemma for resqrex 10954. 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 10937* | Lemma for resqrex 10954. 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 10938* | Lemma for resqrex 10954. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemdec 10939* | Lemma for resqrex 10954. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemdecn 10940* | Lemma for resqrex 10954. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemlo 10941* | Lemma for resqrex 10954. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc1 10942* | Lemma for resqrex 10954. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc2 10943* | Lemma for resqrex 10954. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc3 10944* | Lemma for resqrex 10954. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemnmsq 10945* | Lemma for resqrex 10954. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
Theorem | resqrexlemnm 10946* | Lemma for resqrex 10954. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemcvg 10947* | Lemma for resqrex 10954. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | resqrexlemgt0 10948* | Lemma for resqrex 10954. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemoverl 10949* | Lemma for resqrex 10954. 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 10950* | Lemma for resqrex 10954. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemga 10951* | Lemma for resqrex 10954. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemsqa 10952* | Lemma for resqrex 10954. The square of a limit is . (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemex 10953* | Lemma for resqrex 10954. 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 10954* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | rsqrmo 10955* | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | rersqreu 10956* | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | resqrtcl 10957 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | rersqrtthlem 10958 | Lemma for resqrtth 10959. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | resqrtth 10959 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | remsqsqrt 10960 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrtge0 10961 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrtgt0 10962 | 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 10963 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtle 10964 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtlt 10965 | Square root is strictly monotonic. Closed form of sqrtlti 11065. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | sqrt11ap 10966 | Analogue to sqrt11 10967 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# # | ||
Theorem | sqrt11 10967 | The square root function is one-to-one. Also see sqrt11ap 10966 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 10968 | 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 10969 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
Theorem | sqrtdiv 10970 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
Theorem | sqrtsq2 10971 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtsq 10972 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrtmsq 10973 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | sqrt1 10974 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
Theorem | sqrt4 10975 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
Theorem | sqrt9 10976 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
Theorem | sqrt2gt1lt2 10977 | 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 10978 | Absolute value of negative. (Contributed by NM, 27-Feb-2005.) |
Theorem | abscl 10979 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
Theorem | abscj 10980 | 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 10981 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
Theorem | absvalsq2 10982 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
Theorem | sqabsadd 10983 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) |
Theorem | sqabssub 10984 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
Theorem | absval2 10985 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
Theorem | abs0 10986 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | absi 10987 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
Theorem | absge0 10988 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | absrpclap 10989 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# | ||
Theorem | abs00ap 10990 | 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 10991 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) |
# # | ||
Theorem | abs00 10992 | The absolute value of a number is zero iff the number is zero. Also see abs00ap 10990 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 10993 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 10992. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | abs00bd 10994 | If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.) |
Theorem | absreimsq 10995 | 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 10996 | Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.) |
Theorem | absmul 10997 | 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 10998 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# | ||
Theorem | absid 10999 | A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | abs1 11000 | The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |