Home | Metamath
Proof Explorer Theorem List (p. 140 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjreim2 13901 | The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | cj11 13902 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
Theorem | cjne0 13903 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
Theorem | cjdiv 13904 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
Theorem | cnrecnv 13905* | The inverse to the canonical bijection from to from cnref1o 11827. (Contributed by Mario Carneiro, 25-Aug-2014.) |
Theorem | sqeqd 13906 | A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015.) |
Theorem | recli 13907 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
Theorem | imcli 13908 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
Theorem | cjcli 13909 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
Theorem | replimi 13910 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
Theorem | cjcji 13911 | 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 13912 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
Theorem | rerebi 13913 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
Theorem | cjrebi 13914 | 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 13915 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | imcji 13916 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulrcli 13917 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
Theorem | cjmulvali 13918 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjmulge0i 13919 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
Theorem | renegi 13920 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | imnegi 13921 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | cjnegi 13922 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
Theorem | addcji 13923 | 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 13924 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | imaddi 13925 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
Theorem | remuli 13926 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | immuli 13927 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjaddi 13928 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | cjmuli 13929 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
Theorem | ipcni 13930 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
Theorem | cjdivi 13931 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
Theorem | crrei 13932 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | crimi 13933 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
Theorem | recld 13934 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcld 13935 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjcld 13936 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | replimd 13937 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remimd 13938 | 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 13939 | 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 13940 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rerebd 13941 | 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 13942 | 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 13943 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | recjd 13944 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imcjd 13945 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulrcld 13946 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulvald 13947 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmulge0d 13948 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | renegd 13949 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imnegd 13950 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjnegd 13951 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | addcjd 13952 | 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 13953 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | readdd 13954 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imaddd 13955 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | resubd 13956 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imsubd 13957 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | remuld 13958 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immuld 13959 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjaddd 13960 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjmuld 13961 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | ipcnd 13962 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjdivd 13963 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | rered 13964 | 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 13965 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | cjred 13966 | 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 13967 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | immul2d 13968 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | redivd 13969 | Real part of a division. Related to remul2 13870. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | imdivd 13970 | Imaginary part of a division. Related to remul2 13870. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | crred 13971 | 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 13972 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
Syntax | csqrt 13973 | Extend class notation to include square root of a complex number. |
Syntax | cabs 13974 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
Definition | df-sqrt 13975* |
Define a function whose value is the square root of a complex number.
For example, (ex-sqrt 27311).
Since iff , we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 14101 for its closure, sqrtval 13977 for its value, sqrtth 14104 and sqsqrti 14115 for its relationship to squares, and sqrt11i 14124 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
Definition | df-abs 13976 | Define the function for the absolute value (modulus) of a complex number. See abscli 14134 for its closure and absval 13978 or absval2i 14136 for its value. For example, (ex-abs 27312). (Contributed by NM, 27-Jul-1999.) |
Theorem | sqrtval 13977* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | absval 13978 | 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 13979 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | cnpart 13980 | The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map ). (Contributed by Mario Carneiro, 8-Jul-2013.) |
Theorem | sqr0lem 13981 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrt0 13982 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrlem1 13983* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem2 13984* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem3 13985* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem4 13986* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem5 13987* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem6 13988* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrlem7 13989* | Lemma for 01sqrex 13990. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | 01sqrex 13990* | Existence of a square root for reals in the interval . (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | resqrex 13991* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrmo 13992* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
Theorem | resqreu 13993* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrtcl 13994 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrtthlem 13995 | Lemma for resqrtth 13996. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | resqrtth 13996 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
Theorem | remsqsqrt 13997 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
Theorem | sqrtge0 13998 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
Theorem | sqrtgt0 13999 | 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 14000 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |