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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | shftcan1 14901 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift π΄) shift -π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | shftcan2 14902 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π΄ β β β§ π΅ β β) β (((πΉ shift -π΄) shift π΄)βπ΅) = (πΉβπ΅)) | ||
Theorem | seqshft 14903 | 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 14904 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 14905 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 15886). 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 15886. We define this over β* (df-xr 11126) 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 14906. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ sgn = (π₯ β β* β¦ if(π₯ = 0, 0, if(π₯ < 0, -1, 1))) | ||
Theorem | sgnval 14906 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ β β* β (sgnβπ΄) = if(π΄ = 0, 0, if(π΄ < 0, -1, 1))) | ||
Theorem | sgn0 14907 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (sgnβ0) = 0 | ||
Theorem | sgnp 14908 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ 0 < π΄) β (sgnβπ΄) = 1) | ||
Theorem | sgnrrp 14909 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
β’ (π΄ β β+ β (sgnβπ΄) = 1) | ||
Theorem | sgn1 14910 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ1) = 1 | ||
Theorem | sgnpnf 14911 | The signum of +β is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ+β) = 1 | ||
Theorem | sgnn 14912 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ ((π΄ β β* β§ π΄ < 0) β (sgnβπ΄) = -1) | ||
Theorem | sgnmnf 14913 | The signum of -β is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
β’ (sgnβ-β) = -1 | ||
Syntax | ccj 14914 | Extend class notation to include complex conjugate function. |
class β | ||
Syntax | cre 14915 | Extend class notation to include real part of a complex number. |
class β | ||
Syntax | cim 14916 | Extend class notation to include imaginary part of a complex number. |
class β | ||
Definition | df-cj 14917* | Define the complex conjugate function. See cjcli 14987 for its closure and cjval 14920 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β = (π₯ β β β¦ (β©π¦ β β ((π₯ + π¦) β β β§ (i Β· (π₯ β π¦)) β β))) | ||
Definition | df-re 14918 | Define a function whose value is the real part of a complex number. See reval 14924 for its value, recli 14985 for its closure, and replim 14934 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ ((π₯ + (ββπ₯)) / 2)) | ||
Definition | df-im 14919 | Define a function whose value is the imaginary part of a complex number. See imval 14925 for its value, imcli 14986 for its closure, and replim 14934 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
β’ β = (π₯ β β β¦ (ββ(π₯ / i))) | ||
Theorem | cjval 14920* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) = (β©π₯ β β ((π΄ + π₯) β β β§ (i Β· (π΄ β π₯)) β β))) | ||
Theorem | cjth 14921 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β ((π΄ + (ββπ΄)) β β β§ (i Β· (π΄ β (ββπ΄))) β β)) | ||
Theorem | cjf 14922 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | cjcl 14923 | 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 14924 | 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 14925 | 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 14926 | 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 14927 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
β’ (π΄ β β β (ββπ΄) = (ββ(i Β· π΄))) | ||
Theorem | recl 14928 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | imcl 14929 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ (π΄ β β β (ββπ΄) β β) | ||
Theorem | ref 14930 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | imf 14931 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
β’ β:ββΆβ | ||
Theorem | crre 14932 | 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 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 | replim 14934 | 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 14935 | 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 14936 | 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 14937 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
β’ (π΄ β β β (π΄ β β β (ββπ΄) = 0)) | ||
Theorem | rereb 14938 | 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 14939 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (π΄ β β β (π΅ Β· π΄) β β)) | ||
Theorem | rere 14940 | 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 14941 | 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 14942 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = (ββπ΄)) | ||
Theorem | reneg 14943 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | readd 14944 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | resub 14945 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | remullem 14946 | Lemma for remul 14947, immul 14954, and cjmul 14960. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅))) β§ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | remul 14947 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | remul2 14948 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | rediv 14949 | Real part of a division. Related to remul2 14948. (Contributed by David A. Wheeler, 10-Jun-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) | ||
Theorem | imcj 14950 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ(ββπ΄)) = -(ββπ΄)) | ||
Theorem | imneg 14951 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | imadd 14952 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | imsub 14953 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | immul 14954 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | immul2 14955 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | imdiv 14956 | Imaginary part of a division. Related to immul2 14955. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / π΅)) | ||
Theorem | cjre 14957 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjcj 14958 | 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 14959 | 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 14960 | 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 14961 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ Β· (ββπ΅))) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | cjmulrcl 14962 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ Β· (ββπ΄)) β β) | ||
Theorem | cjmulval 14963 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | cjmulge0 14964 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β 0 β€ (π΄ Β· (ββπ΄))) | ||
Theorem | cjneg 14965 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
β’ (π΄ β β β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | addcj 14966 | 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 14967 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | cjexp 14968 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
β’ ((π΄ β β β§ π β β0) β (ββ(π΄βπ)) = ((ββπ΄)βπ)) | ||
Theorem | imval2 14969 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (ββπ΄) = ((π΄ β (ββπ΄)) / (2 Β· i))) | ||
Theorem | re0 14970 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | im0 14971 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | re1 14972 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 1 | ||
Theorem | im1 14973 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 0 | ||
Theorem | rei 14974 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 0 | ||
Theorem | imi 14975 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 1 | ||
Theorem | cj0 14976 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | cji 14977 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
β’ (ββi) = -i | ||
Theorem | cjreim 14978 | 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 14979 | 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 14980 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | cjne0 14981 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
β’ (π΄ β β β (π΄ β 0 β (ββπ΄) β 0)) | ||
Theorem | cjdiv 14982 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ β 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | cnrecnv 14983* | The inverse to the canonical bijection from (β Γ β) to β from cnref1o 12838. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) β β’ β‘πΉ = (π§ β β β¦ β¨(ββπ§), (ββπ§)β©) | ||
Theorem | sqeqd 14984 | 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 14985 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | imcli 14986 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | cjcli 14987 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | replimi 14988 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β β β’ π΄ = ((ββπ΄) + (i Β· (ββπ΄))) | ||
Theorem | cjcji 14989 | 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 14990 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = 0) | ||
Theorem | rerebi 14991 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjrebi 14992 | 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 14993 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = (ββπ΄) | ||
Theorem | imcji 14994 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = -(ββπ΄) | ||
Theorem | cjmulrcli 14995 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) β β | ||
Theorem | cjmulvali 14996 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2)) | ||
Theorem | cjmulge0i 14997 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
β’ π΄ β β β β’ 0 β€ (π΄ Β· (ββπ΄)) | ||
Theorem | renegi 14998 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | imnegi 14999 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | cjnegi 15000 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |