Home | Intuitionistic Logic Explorer Theorem List (p. 108 of 133) | < 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 | imaddi 10701 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | remuli 10702 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | immuli 10703 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjaddi 10704 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjmuli 10705 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | ipcni 10706 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjdivapi 10707 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
Theorem | crrei 10708 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | crimi 10709 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | recld 10710 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcld 10711 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcld 10712 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | replimd 10713 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remimd 10714 | Value of the conjugate of a complex number. The value is the real part minus times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcjd 10715 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | reim0bd 10716 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rerebd 10717 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjrebd 10718 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjne0d 10719 | A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 10720 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjap0d 10720 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
# # | ||
Theorem | recjd 10721 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcjd 10722 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulrcld 10723 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulvald 10724 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulge0d 10725 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | renegd 10726 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imnegd 10727 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjnegd 10728 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | addcjd 10729 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjexpd 10730 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | readdd 10731 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imaddd 10732 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | resubd 10733 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imsubd 10734 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remuld 10735 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immuld 10736 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjaddd 10737 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmuld 10738 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | ipcnd 10739 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjdivapd 10740 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | rered 10741 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | reim0d 10742 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjred 10743 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remul2d 10744 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immul2d 10745 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | redivapd 10746 | Real part of a division. Related to remul2 10645. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | imdivapd 10747 | Imaginary part of a division. Related to remul2 10645. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | crred 10748 | 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 10749 | 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 10750 | Complex apartness in terms of real and imaginary parts. See also apreim 8365 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
Theorem | caucvgrelemrec 10751* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
# | ||
Theorem | caucvgrelemcau 10752* | Lemma for caucvgre 10753. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
Theorem | caucvgre 10753* |
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 10754 | Lemma for cvg1n 10758. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | cvg1nlemf 10755* | Lemma for cvg1n 10758. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemcau 10756* | Lemma for cvg1n 10758. 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 10757* | Lemma for cvg1n 10758. 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 10758* |
Convergence of real sequences.
This is a version of caucvgre 10753 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 10759 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | rexanuz 10760* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
Theorem | rexfiuz 10761* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
Theorem | rexuz3 10762* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | rexanuz2 10763* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | r19.29uz 10764* | A version of 19.29 1599 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
Theorem | r19.2uz 10765* | A version of r19.2m 3449 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
Theorem | recvguniqlem 10766 | Lemma for recvguniq 10767. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Theorem | recvguniq 10767* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Syntax | csqrt 10768 | Extend class notation to include square root of a complex number. |
Syntax | cabs 10769 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-rsqrt 10770* |
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 10771 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtrval 10772* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Theorem | absval 10773 | 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 10774 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | sqrt0rlem 10775 | Lemma for sqrt0 10776. (Contributed by Jim Kingdon, 26-Aug-2020.) |
Theorem | sqrt0 10776 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrexlem1arp 10777 | Lemma for resqrex 10798. is a positive real (expressed in a way that will help apply seqf 10234 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemp1rp 10778* | Lemma for resqrex 10798. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10234 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf 10779* | Lemma for resqrex 10798. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
Theorem | resqrexlemf1 10780* | Lemma for resqrex 10798. 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 10781* | Lemma for resqrex 10798. 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 10782* | Lemma for resqrex 10798. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemdec 10783* | Lemma for resqrex 10798. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemdecn 10784* | Lemma for resqrex 10798. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemlo 10785* | Lemma for resqrex 10798. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc1 10786* | Lemma for resqrex 10798. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc2 10787* | Lemma for resqrex 10798. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc3 10788* | Lemma for resqrex 10798. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemnmsq 10789* | Lemma for resqrex 10798. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
Theorem | resqrexlemnm 10790* | Lemma for resqrex 10798. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemcvg 10791* | Lemma for resqrex 10798. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | resqrexlemgt0 10792* | Lemma for resqrex 10798. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemoverl 10793* | Lemma for resqrex 10798. 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 10794* | Lemma for resqrex 10798. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemga 10795* | Lemma for resqrex 10798. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
Theorem | resqrexlemsqa 10796* | Lemma for resqrex 10798. The square of a limit is . (Contributed by Jim Kingdon, 7-Aug-2021.) |
Theorem | resqrexlemex 10797* | Lemma for resqrex 10798. 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 10798* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | rsqrmo 10799* | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
Theorem | rersqreu 10800* | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |