![]() |
Metamath
Proof Explorer Theorem List (p. 144 of 437) | < 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: | ![]() (1-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | addcj 14301 | 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 14302 | Complex conjugate distributes over subtraction. (Contributed by NM, 28-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵))) | ||
Theorem | cjexp 14303 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | imval2 14304 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = ((𝐴 − (∗‘𝐴)) / (2 · i))) | ||
Theorem | re0 14305 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℜ‘0) = 0 | ||
Theorem | im0 14306 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (ℑ‘0) = 0 | ||
Theorem | re1 14307 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℜ‘1) = 1 | ||
Theorem | im1 14308 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘1) = 0 | ||
Theorem | rei 14309 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℜ‘i) = 0 | ||
Theorem | imi 14310 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
⊢ (ℑ‘i) = 1 | ||
Theorem | cj0 14311 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
⊢ (∗‘0) = 0 | ||
Theorem | cji 14312 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (∗‘i) = -i | ||
Theorem | cjreim 14313 | 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 14314 | 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 14315 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) = (∗‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | cjne0 14316 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0)) | ||
Theorem | cjdiv 14317 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | cnrecnv 14318* | The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 12137. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ 〈(ℜ‘𝑧), (ℑ‘𝑧)〉) | ||
Theorem | sqeqd 14319 | 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 14320 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ∈ ℝ | ||
Theorem | imcli 14321 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘𝐴) ∈ ℝ | ||
Theorem | cjcli 14322 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘𝐴) ∈ ℂ | ||
Theorem | replimi 14323 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) | ||
Theorem | cjcji 14324 | 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 14325 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) | ||
Theorem | rerebi 14326 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) | ||
Theorem | cjrebi 14327 | 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 14328 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) | ||
Theorem | imcji 14329 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) | ||
Theorem | cjmulrcli 14330 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ | ||
Theorem | cjmulvali 14331 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | cjmulge0i 14332 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) | ||
Theorem | renegi 14333 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) | ||
Theorem | imnegi 14334 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴) | ||
Theorem | cjnegi 14335 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘-𝐴) = -(∗‘𝐴) | ||
Theorem | addcji 14336 | 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 14337 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)) | ||
Theorem | imaddi 14338 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)) | ||
Theorem | remuli 14339 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | immuli 14340 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) | ||
Theorem | cjaddi 14341 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)) | ||
Theorem | cjmuli 14342 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)) | ||
Theorem | ipcni 14343 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | cjdivi 14344 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | crrei 14345 | 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 14346 | 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 14347 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcld 14348 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | cjcld 14349 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ) | ||
Theorem | replimd 14350 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) | ||
Theorem | remimd 14351 | 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 14352 | 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 14353 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℑ‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rerebd 14354 | 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 14355 | 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 14356 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) ≠ 0) | ||
Theorem | recjd 14357 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | imcjd 14358 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | cjmulrcld 14359 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulvald 14360 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0d 14361 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | renegd 14362 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | imnegd 14363 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | cjnegd 14364 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcjd 14365 | 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 14366 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | readdd 14367 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | imaddd 14368 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | resubd 14369 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | imsubd 14370 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | remuld 14371 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | immuld 14372 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | cjaddd 14373 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) | ||
Theorem | cjmuld 14374 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) | ||
Theorem | ipcnd 14375 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjdivd 14376 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | rered 14377 | 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 14378 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) = 0) | ||
Theorem | cjred 14379 | 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 14380 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | immul2d 14381 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | redivd 14382 | Real part of a division. Related to remul2 14283. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴)) | ||
Theorem | imdivd 14383 | Imaginary part of a division. Related to remul2 14283. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴)) | ||
Theorem | crred 14384 | 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 14385 | 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 14386 | Extend class notation to include square root of a complex number. |
class √ | ||
Syntax | cabs 14387 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-sqrt 14388* |
Define a function whose value is the square root of a complex number.
For example, (√‘25) = 5 (ex-sqrt 27903).
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. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 14515 for its closure, sqrtval 14390 for its value, sqrtth 14518 and sqsqrti 14529 for its relationship to squares, and sqrt11i 14538 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) | ||
Definition | df-abs 14389 | Define the function for the absolute value (modulus) of a complex number. See abscli 14549 for its closure and absval 14391 or absval2i 14551 for its value. For example, (abs‘-2) = 2 (ex-abs 27904). (Contributed by NM, 27-Jul-1999.) |
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) | ||
Theorem | sqrtval 14390* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))) | ||
Theorem | absval 14391 | 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 14392 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+) | ||
Theorem | cnpart 14393 | 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 14394 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ (ℜ‘𝐴) ∧ (i · 𝐴) ∉ ℝ+)) ↔ 𝐴 = 0) | ||
Theorem | sqrt0 14395 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (√‘0) = 0 | ||
Theorem | sqrlem1 14396* | Lemma for 01sqrex 14403. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1) | ||
Theorem | sqrlem2 14397* | Lemma for 01sqrex 14403. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆) | ||
Theorem | sqrlem3 14398* | Lemma for 01sqrex 14403. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧)) | ||
Theorem | sqrlem4 14399* | Lemma for 01sqrex 14403. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) | ||
Theorem | sqrlem5 14400* | Lemma for 01sqrex 14403. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |