Home | Metamath
Proof Explorer Theorem List (p. 150 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | shftidt 14901 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ (π΄ β β β ((πΉ shift 0)βπ΄) = (πΉβπ΄)) | ||
Theorem | shftcan1 14902 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift π΄) shift -π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | shftcan2 14903 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift -π΄) shift π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | seqshft 14904 | Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-Feb-2014.) |
β’ πΉ β V β β’ ((π β β€ β§ π β β€) β seqπ( + , (πΉ shift π)) = (seq(π β π)( + , πΉ) shift π)) | ||
Syntax | csgn 14905 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 14906 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 15887). Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4 15887. We define this over β* (df-xr 11127) instead of β so that it can accept +β and -β. Note that df-psgn 19205 defines the sign of a permutation, which is different. Value shown in sgnval 14907. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ sgn = (π₯ β β* β¦ if(π₯ = 0, 0, if(π₯ < 0, -1, 1))) | ||
Theorem | sgnval 14907 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ β β* β (sgnβπ΄) = if(π΄ = 0, 0, if(π΄ < 0, -1, 1))) | ||
Theorem | sgn0 14908 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (sgnβ0) = 0 | ||
Theorem | sgnp 14909 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (sgnβπ΄) = 1) | ||
Theorem | sgnrrp 14910 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
β’ (π΄ β β+ β (sgnβπ΄) = 1) | ||
Theorem | sgn1 14911 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ1) = 1 | ||
Theorem | sgnpnf 14912 | The signum of +β is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ+β) = 1 | ||
Theorem | sgnn 14913 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ π΄ < 0) β (sgnβπ΄) = -1) | ||
Theorem | sgnmnf 14914 | The signum of -β is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ-β) = -1 | ||
Syntax | ccj 14915 | Extend class notation to include complex conjugate function. |
class β | ||
Syntax | cre 14916 | Extend class notation to include real part of a complex number. |
class β | ||
Syntax | cim 14917 | Extend class notation to include imaginary part of a complex number. |
class β | ||
Definition | df-cj 14918* | Define the complex conjugate function. See cjcli 14988 for its closure and cjval 14921 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β = (π₯ β β β¦ (β©π¦ β β ((π₯ + π¦) β β β§ (i Β· (π₯ β π¦)) β β))) | ||
Definition | df-re 14919 | Define a function whose value is the real part of a complex number. See reval 14925 for its value, recli 14986 for its closure, and replim 14935 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ ((π₯ + (ββπ₯)) / 2)) | ||
Definition | df-im 14920 | Define a function whose value is the imaginary part of a complex number. See imval 14926 for its value, imcli 14987 for its closure, and replim 14935 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ (ββ(π₯ / i))) | ||
Theorem | cjval 14921* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (β©π₯ β β ((π΄ + π₯) β β β§ (i Β· (π΄ β π₯)) β β))) | ||
Theorem | cjth 14922 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β ((π΄ + (ββπ΄)) β β β§ (i Β· (π΄ β (ββπ΄))) β β)) | ||
Theorem | cjf 14923 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | cjcl 14924 | The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | reval 14925 | The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = ((π΄ + (ββπ΄)) / 2)) | ||
Theorem | imval 14926 | The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (ββ(π΄ / i))) | ||
Theorem | imre 14927 | The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (ββ(-i Β· π΄))) | ||
Theorem | reim 14928 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π΄ β β β (ββπ΄) = (ββ(i Β· π΄))) | ||
Theorem | recl 14929 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | imcl 14930 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | ref 14931 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | imf 14932 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | crre 14933 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = π΄) | ||
Theorem | crim 14934 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = π΅) | ||
Theorem | replim 14935 | Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β π΄ = ((ββπ΄) + (i Β· (ββπ΄)))) | ||
Theorem | remim 14936 | Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = ((ββπ΄) β (i Β· (ββπ΄)))) | ||
Theorem | reim0 14937 | The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = 0) | ||
Theorem | reim0b 14938 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = 0)) | ||
Theorem | rereb 14939 | A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = π΄)) | ||
Theorem | mulre 14940 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄ β β β (π΅ Β· π΄) β β)) | ||
Theorem | rere 14941 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Paul Chapman, 7-Sep-2007.) |
β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjreb 14942 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = π΄)) | ||
Theorem | recj 14943 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = (ββπ΄)) | ||
Theorem | reneg 14944 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | readd 14945 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | resub 14946 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | remullem 14947 | Lemma for remul 14948, immul 14955, and cjmul 14961. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | remul 14948 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | remul2 14949 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | rediv 14950 | Real part of a division. Related to remul2 14949. (Contributed by David A. Wheeler, 10-Jun-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) | ||
Theorem | imcj 14951 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = -(ββπ΄)) | ||
Theorem | imneg 14952 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | imadd 14953 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | imsub 14954 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | immul 14955 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | immul2 14956 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | imdiv 14957 | Imaginary part of a division. Related to immul2 14956. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) | ||
Theorem | cjre 14958 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjcj 14959 | The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = π΄) | ||
Theorem | cjadd 14960 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | cjmul 14961 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | ipcnval 14962 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· (ββπ΅))) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | cjmulrcl 14963 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ Β· (ββπ΄)) β β) | ||
Theorem | cjmulval 14964 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | cjmulge0 14965 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β 0 β€ (π΄ Β· (ββπ΄))) | ||
Theorem | cjneg 14966 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | addcj 14967 | A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ + (ββπ΄)) = (2 Β· (ββπ΄))) | ||
Theorem | cjsub 14968 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | cjexp 14969 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
β’ ((π΄ β β β§ π β β0) β (ββ(π΄βπ)) = ((ββπ΄)βπ)) | ||
Theorem | imval2 14970 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (ββπ΄) = ((π΄ β (ββπ΄)) / (2 Β· i))) | ||
Theorem | re0 14971 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | im0 14972 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | re1 14973 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 1 | ||
Theorem | im1 14974 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 0 | ||
Theorem | rei 14975 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 0 | ||
Theorem | imi 14976 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 1 | ||
Theorem | cj0 14977 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | cji 14978 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
β’ (ββi) = -i | ||
Theorem | cjreim 14979 | The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = (π΄ β (i Β· π΅))) | ||
Theorem | cjreim2 14980 | 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.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β (i Β· π΅))) = (π΄ + (i Β· π΅))) | ||
Theorem | cj11 14981 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | cjne0 14982 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
β’ (π΄ β β β (π΄ β 0 β (ββπ΄) β 0)) | ||
Theorem | cjdiv 14983 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | cnrecnv 14984* | The inverse to the canonical bijection from (β Γ β) to β from cnref1o 12839. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) β β’ β‘πΉ = (π§ β β β¦ β¨(ββπ§), (ββπ§)β©) | ||
Theorem | sqeqd 14985 | A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄β2) = (π΅β2)) & β’ (π β 0 β€ (ββπ΄)) & β’ (π β 0 β€ (ββπ΅)) & β’ ((π β§ (ββπ΄) = 0 β§ (ββπ΅) = 0) β π΄ = π΅) β β’ (π β π΄ = π΅) | ||
Theorem | recli 14986 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | imcli 14987 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | cjcli 14988 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | replimi 14989 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β β β’ π΄ = ((ββπ΄) + (i Β· (ββπ΄))) | ||
Theorem | cjcji 14990 | 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 14991 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = 0) | ||
Theorem | rerebi 14992 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjrebi 14993 | 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 14994 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = (ββπ΄) | ||
Theorem | imcji 14995 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = -(ββπ΄) | ||
Theorem | cjmulrcli 14996 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) β β | ||
Theorem | cjmulvali 14997 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2)) | ||
Theorem | cjmulge0i 14998 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
β’ π΄ β β β β’ 0 β€ (π΄ Β· (ββπ΄)) | ||
Theorem | renegi 14999 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | imnegi 15000 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |