Home | Metamath
Proof Explorer Theorem List (p. 148 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | im1 14701 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘1) = 0 | ||
Theorem | rei 14702 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℜ‘i) = 0 | ||
Theorem | imi 14703 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘i) = 1 | ||
Theorem | cj0 14704 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (∗‘0) = 0 | ||
Theorem | cji 14705 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (∗‘i) = -i | ||
Theorem | cjreim 14706 | 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 14707 | 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 14708 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | cjne0 14709 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0)) | ||
Theorem | cjdiv 14710 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | cnrecnv 14711* | The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 12564. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ 〈(ℜ‘𝑧), (ℑ‘𝑧)〉) | ||
Theorem | sqeqd 14712 | 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 14713 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ∈ ℝ | ||
Theorem | imcli 14714 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘𝐴) ∈ ℝ | ||
Theorem | cjcli 14715 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘𝐴) ∈ ℂ | ||
Theorem | replimi 14716 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) | ||
Theorem | cjcji 14717 | 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 14718 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) | ||
Theorem | rerebi 14719 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) | ||
Theorem | cjrebi 14720 | 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 14721 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) | ||
Theorem | imcji 14722 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) | ||
Theorem | cjmulrcli 14723 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ | ||
Theorem | cjmulvali 14724 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | cjmulge0i 14725 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) | ||
Theorem | renegi 14726 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) | ||
Theorem | imnegi 14727 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴) | ||
Theorem | cjnegi 14728 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘-𝐴) = -(∗‘𝐴) | ||
Theorem | addcji 14729 | 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.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)) | ||
Theorem | readdi 14730 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)) | ||
Theorem | imaddi 14731 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)) | ||
Theorem | remuli 14732 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | immuli 14733 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) | ||
Theorem | cjaddi 14734 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)) | ||
Theorem | cjmuli 14735 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)) | ||
Theorem | ipcni 14736 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | cjdivi 14737 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | crrei 14738 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴 | ||
Theorem | crimi 14739 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵 | ||
Theorem | recld 14740 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcld 14741 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | cjcld 14742 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ) | ||
Theorem | replimd 14743 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) | ||
Theorem | remimd 14744 | 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 Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) | ||
Theorem | cjcjd 14745 | 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 14746 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℑ‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rerebd 14747 | 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 14748 | 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 14749 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) ≠ 0) | ||
Theorem | recjd 14750 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | imcjd 14751 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | cjmulrcld 14752 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulvald 14753 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0d 14754 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | renegd 14755 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | imnegd 14756 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | cjnegd 14757 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcjd 14758 | 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.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))) | ||
Theorem | cjexpd 14759 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | readdd 14760 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | imaddd 14761 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | resubd 14762 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | imsubd 14763 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | remuld 14764 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | immuld 14765 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | cjaddd 14766 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) | ||
Theorem | cjmuld 14767 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) | ||
Theorem | ipcnd 14768 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjdivd 14769 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | rered 14770 | 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 14771 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) = 0) | ||
Theorem | cjred 14772 | 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 14773 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | immul2d 14774 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | redivd 14775 | Real part of a division. Related to remul2 14676. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴)) | ||
Theorem | imdivd 14776 | Imaginary part of a division. Related to remul2 14676. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴)) | ||
Theorem | crred 14777 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴) | ||
Theorem | crimd 14778 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵) | ||
Syntax | csqrt 14779 | Extend class notation to include square root of a complex number. |
class √ | ||
Syntax | cabs 14780 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 14781* |
Define a function whose value is the square root of a complex number.
For example, (√‘25) = 5 (ex-sqrt 28509).
Since (𝑦↑2) = 𝑥 iff (-𝑦↑2) = 𝑥, 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 28509. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 14908 for its closure, sqrtval 14783 for its value, sqrtth 14911 and sqsqrti 14922 for its relationship to squares, and sqrt11i 14931 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) | ||
Definition | df-abs 14782 | Define the function for the absolute value (modulus) of a complex number. See abscli 14942 for its closure and absval 14784 or absval2i 14944 for its value. For example, (abs‘-2) = 2 (ex-abs 28510). (Contributed by NM, 27-Jul-1999.) |
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) | ||
Theorem | sqrtval 14783* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))) | ||
Theorem | absval 14784 | 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.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(𝐴 · (∗‘𝐴)))) | ||
Theorem | rennim 14785 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+) | ||
Theorem | cnpart 14786 | 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((0 ≤ (ℜ‘𝐴) ∧ (i · 𝐴) ∉ ℝ+) ↔ ¬ (0 ≤ (ℜ‘-𝐴) ∧ (i · -𝐴) ∉ ℝ+))) | ||
Theorem | sqr0lem 14787 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ (ℜ‘𝐴) ∧ (i · 𝐴) ∉ ℝ+)) ↔ 𝐴 = 0) | ||
Theorem | sqrt0 14788 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (√‘0) = 0 | ||
Theorem | sqrlem1 14789* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1) | ||
Theorem | sqrlem2 14790* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆) | ||
Theorem | sqrlem3 14791* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧)) | ||
Theorem | sqrlem4 14792* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) | ||
Theorem | sqrlem5 14793* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < ))) | ||
Theorem | sqrlem6 14794* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴) | ||
Theorem | sqrlem7 14795* | Lemma for 01sqrex 14796. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴) | ||
Theorem | 01sqrex 14796* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴)) | ||
Theorem | resqrex 14797* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴)) | ||
Theorem | sqrmo 14798* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
⊢ (𝐴 ∈ ℂ → ∃*𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | resqreu 14799* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | resqrtcl 14800 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |