Home | Intuitionistic Logic Explorer Theorem List (p. 99 of 108) | < 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 | replimi 9801 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
Theorem | cjcji 9802 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.) |
Theorem | reim0bi 9803 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
Theorem | rerebi 9804 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
Theorem | cjrebi 9805 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) |
Theorem | recji 9806 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | imcji 9807 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulrcli 9808 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
Theorem | cjmulvali 9809 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulge0i 9810 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
Theorem | renegi 9811 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | imnegi 9812 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | cjnegi 9813 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | addcji 9814 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
Theorem | readdi 9815 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | imaddi 9816 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | remuli 9817 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | immuli 9818 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjaddi 9819 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjmuli 9820 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | ipcni 9821 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjdivapi 9822 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
Theorem | crrei 9823 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | crimi 9824 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | recld 9825 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcld 9826 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcld 9827 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | replimd 9828 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remimd 9829 | 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 9830 | 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 9831 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rerebd 9832 | 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 9833 | 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 9834 | A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 9835 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjap0d 9835 | 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 9836 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcjd 9837 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulrcld 9838 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulvald 9839 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulge0d 9840 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | renegd 9841 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imnegd 9842 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjnegd 9843 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | addcjd 9844 | 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 9845 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | readdd 9846 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imaddd 9847 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | resubd 9848 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imsubd 9849 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remuld 9850 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immuld 9851 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjaddd 9852 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmuld 9853 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | ipcnd 9854 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjdivapd 9855 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | rered 9856 | 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 9857 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjred 9858 | 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 9859 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immul2d 9860 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | redivapd 9861 | Real part of a division. Related to remul2 9760. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | imdivapd 9862 | Imaginary part of a division. Related to remul2 9760. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
Theorem | crred 9863 | 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 9864 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | caucvgrelemrec 9865* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
# | ||
Theorem | caucvgrelemcau 9866* | Lemma for caucvgre 9867. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
Theorem | caucvgre 9867* |
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 9868 | Lemma for cvg1n 9872. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
Theorem | cvg1nlemf 9869* | Lemma for cvg1n 9872. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
Theorem | cvg1nlemcau 9870* | Lemma for cvg1n 9872. 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 9871* | Lemma for cvg1n 9872. 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 9872* |
Convergence of real sequences.
This is a version of caucvgre 9867 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 9873 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | rexanuz 9874* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
Theorem | rexfiuz 9875* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
Theorem | rexuz3 9876* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | rexanuz2 9877* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | r19.29uz 9878* | A version of 19.29 1551 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
Theorem | r19.2uz 9879* | A version of r19.2m 3329 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
Theorem | recvguniqlem 9880 | Lemma for recvguniq 9881. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
Theorem | recvguniq 9881* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
Syntax | csqrt 9882 | Extend class notation to include square root of a complex number. |
Syntax | cabs 9883 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-rsqrt 9884* |
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 9885 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtrval 9886* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
Theorem | absval 9887 | 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 9888 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | sqrt0rlem 9889 | Lemma for sqrt0 9890. (Contributed by Jim Kingdon, 26-Aug-2020.) |
Theorem | sqrt0 9890 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrexlem1arp 9891* | Lemma for resqrex 9912. is a positive real (expressed in a way that will help apply iseqf 9444 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) |
Theorem | resqrexlemp1rp 9892* | Lemma for resqrex 9912. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9444 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) |
Theorem | resqrexlemf 9893* | Lemma for resqrex 9912. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemf1 9894* | Lemma for resqrex 9912. 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.) |
Theorem | resqrexlemfp1 9895* | Lemma for resqrex 9912. 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 9896* | Lemma for resqrex 9912. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
Theorem | resqrexlemdec 9897* | Lemma for resqrex 9912. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemdecn 9898* | Lemma for resqrex 9912. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
Theorem | resqrexlemlo 9899* | Lemma for resqrex 9912. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
Theorem | resqrexlemcalc1 9900* | Lemma for resqrex 9912. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |