Home | Metamath
Proof Explorer Theorem List (p. 149 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | shftidt2 14801 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 shift 0) = (𝐹 ↾ ℂ) | ||
Theorem | shftidt 14802 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐴 ∈ ℂ → ((𝐹 shift 0)‘𝐴) = (𝐹‘𝐴)) | ||
Theorem | shftcan1 14803 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift 𝐴) shift -𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | shftcan2 14804 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐹 shift -𝐴) shift 𝐴)‘𝐵) = (𝐹‘𝐵)) | ||
Theorem | seqshft 14805 | 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 14806 | Extend class notation to include the Signum function. |
class sgn | ||
Definition | df-sgn 14807 | Signum function. We do not call it "sign", which is homophonic with "sine" (df-sin 15788). 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 15788. We define this over ℝ* (df-xr 11022) instead of ℝ so that it can accept +∞ and -∞. Note that df-psgn 19108 defines the sign of a permutation, which is different. Value shown in sgnval 14808. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ sgn = (𝑥 ∈ ℝ* ↦ if(𝑥 = 0, 0, if(𝑥 < 0, -1, 1))) | ||
Theorem | sgnval 14808 | Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) | ||
Theorem | sgn0 14809 | The signum of 0 is 0. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ (sgn‘0) = 0 | ||
Theorem | sgnp 14810 | The signum of a positive extended real is 1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 0 < 𝐴) → (sgn‘𝐴) = 1) | ||
Theorem | sgnrrp 14811 | The signum of a positive real is 1. (Contributed by David A. Wheeler, 18-May-2015.) |
⊢ (𝐴 ∈ ℝ+ → (sgn‘𝐴) = 1) | ||
Theorem | sgn1 14812 | The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘1) = 1 | ||
Theorem | sgnpnf 14813 | The signum of +∞ is 1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘+∞) = 1 | ||
Theorem | sgnn 14814 | The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐴 < 0) → (sgn‘𝐴) = -1) | ||
Theorem | sgnmnf 14815 | The signum of -∞ is -1. (Contributed by David A. Wheeler, 26-Jun-2016.) |
⊢ (sgn‘-∞) = -1 | ||
Syntax | ccj 14816 | Extend class notation to include complex conjugate function. |
class ∗ | ||
Syntax | cre 14817 | Extend class notation to include real part of a complex number. |
class ℜ | ||
Syntax | cim 14818 | Extend class notation to include imaginary part of a complex number. |
class ℑ | ||
Definition | df-cj 14819* | Define the complex conjugate function. See cjcli 14889 for its closure and cjval 14822 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) | ||
Definition | df-re 14820 | Define a function whose value is the real part of a complex number. See reval 14826 for its value, recli 14887 for its closure, and replim 14836 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℜ = (𝑥 ∈ ℂ ↦ ((𝑥 + (∗‘𝑥)) / 2)) | ||
Definition | df-im 14821 | Define a function whose value is the imaginary part of a complex number. See imval 14827 for its value, imcli 14888 for its closure, and replim 14836 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
⊢ ℑ = (𝑥 ∈ ℂ ↦ (ℜ‘(𝑥 / i))) | ||
Theorem | cjval 14822* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))) | ||
Theorem | cjth 14823 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + (∗‘𝐴)) ∈ ℝ ∧ (i · (𝐴 − (∗‘𝐴))) ∈ ℝ)) | ||
Theorem | cjf 14824 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
⊢ ∗:ℂ⟶ℂ | ||
Theorem | cjcl 14825 | 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 14826 | 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 14827 | 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 14828 | 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 14829 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) = (ℑ‘(i · 𝐴))) | ||
Theorem | recl 14830 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcl 14831 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | ref 14832 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℜ:ℂ⟶ℝ | ||
Theorem | imf 14833 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
⊢ ℑ:ℂ⟶ℝ | ||
Theorem | crre 14834 | 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 14835 | 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 14836 | 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 14837 | 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 14838 | 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 14839 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0)) | ||
Theorem | rereb 14840 | 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 14841 | A product with a nonzero real multiplier is real iff the multiplicand is real. (Contributed by NM, 21-Aug-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℝ ↔ (𝐵 · 𝐴) ∈ ℝ)) | ||
Theorem | rere 14842 | 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 14843 | 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 14844 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | reneg 14845 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | readd 14846 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | resub 14847 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | remullem 14848 | Lemma for remul 14849, immul 14856, and cjmul 14862. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) ∧ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) ∧ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))) | ||
Theorem | remul 14849 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | remul2 14850 | Real part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | rediv 14851 | Real part of a division. Related to remul2 14850. (Contributed by David A. Wheeler, 10-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℜ‘(𝐴 / 𝐵)) = ((ℜ‘𝐴) / 𝐵)) | ||
Theorem | imcj 14852 | Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | imneg 14853 | The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | imadd 14854 | Imaginary part distributes over addition. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | imsub 14855 | Imaginary part distributes over subtraction. (Contributed by NM, 18-Mar-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | immul 14856 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | immul2 14857 | Imaginary part of a product. (Contributed by Mario Carneiro, 2-Aug-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | imdiv 14858 | Imaginary part of a division. Related to immul2 14857. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (ℑ‘(𝐴 / 𝐵)) = ((ℑ‘𝐴) / 𝐵)) | ||
Theorem | cjre 14859 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → (∗‘𝐴) = 𝐴) | ||
Theorem | cjcj 14860 | 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 14861 | 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 14862 | 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 14863 | Standard inner product on complex numbers. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjmulrcl 14864 | A complex number times its conjugate is real. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulval 14865 | A complex number times its conjugate. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0 14866 | A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | cjneg 14867 | Complex conjugate of negative. (Contributed by NM, 27-Feb-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℂ → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcj 14868 | 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 14869 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵))) | ||
Theorem | cjexp 14870 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | imval2 14871 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) | ||
Theorem | re0 14872 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℜ‘0) = 0 | ||
Theorem | im0 14873 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℑ‘0) = 0 | ||
Theorem | re1 14874 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℜ‘1) = 1 | ||
Theorem | im1 14875 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘1) = 0 | ||
Theorem | rei 14876 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℜ‘i) = 0 | ||
Theorem | imi 14877 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘i) = 1 | ||
Theorem | cj0 14878 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (∗‘0) = 0 | ||
Theorem | cji 14879 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (∗‘i) = -i | ||
Theorem | cjreim 14880 | 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 14881 | 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 14882 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | cjne0 14883 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0)) | ||
Theorem | cjdiv 14884 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | cnrecnv 14885* | The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 12734. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ 〈(ℜ‘𝑧), (ℑ‘𝑧)〉) | ||
Theorem | sqeqd 14886 | 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 14887 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ∈ ℝ | ||
Theorem | imcli 14888 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘𝐴) ∈ ℝ | ||
Theorem | cjcli 14889 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘𝐴) ∈ ℂ | ||
Theorem | replimi 14890 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) | ||
Theorem | cjcji 14891 | 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 14892 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) | ||
Theorem | rerebi 14893 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) | ||
Theorem | cjrebi 14894 | 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 14895 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) | ||
Theorem | imcji 14896 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) | ||
Theorem | cjmulrcli 14897 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ | ||
Theorem | cjmulvali 14898 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | cjmulge0i 14899 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) | ||
Theorem | renegi 14900 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |