![]() |
Intuitionistic Logic Explorer Theorem List (p. 105 of 122) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjap 10401 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((∗‘𝐴) # (∗‘𝐵) ↔ 𝐴 # 𝐵)) | ||
Theorem | cjap0 10402 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ (∗‘𝐴) # 0)) | ||
Theorem | cjne0 10403 | A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 10402 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ (∗‘𝐴) ≠ 0)) | ||
Theorem | cjdivap 10404 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | cnrecnv 10405* | The inverse to the canonical bijection from (ℝ × ℝ) to ℂ from cnref1o 9194. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ◡𝐹 = (𝑧 ∈ ℂ ↦ 〈(ℜ‘𝑧), (ℑ‘𝑧)〉) | ||
Theorem | recli 10406 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ∈ ℝ | ||
Theorem | imcli 10407 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘𝐴) ∈ ℝ | ||
Theorem | cjcli 10408 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘𝐴) ∈ ℂ | ||
Theorem | replimi 10409 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) | ||
Theorem | cjcji 10410 | 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 10411 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) | ||
Theorem | rerebi 10412 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) | ||
Theorem | cjrebi 10413 | 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 10414 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) | ||
Theorem | imcji 10415 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) | ||
Theorem | cjmulrcli 10416 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ | ||
Theorem | cjmulvali 10417 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | cjmulge0i 10418 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) | ||
Theorem | renegi 10419 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) | ||
Theorem | imnegi 10420 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴) | ||
Theorem | cjnegi 10421 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘-𝐴) = -(∗‘𝐴) | ||
Theorem | addcji 10422 | 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 10423 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)) | ||
Theorem | imaddi 10424 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)) | ||
Theorem | remuli 10425 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | immuli 10426 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) | ||
Theorem | cjaddi 10427 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)) | ||
Theorem | cjmuli 10428 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)) | ||
Theorem | ipcni 10429 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
Theorem | cjdivapi 10430 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 # 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | crrei 10431 | 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 10432 | 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 10433 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ) | ||
Theorem | imcld 10434 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) | ||
Theorem | cjcld 10435 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ) | ||
Theorem | replimd 10436 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) | ||
Theorem | remimd 10437 | 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 10438 | 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 10439 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℑ‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rerebd 10440 | 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 10441 | 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 10442 | A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 10443 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) ≠ 0) | ||
Theorem | cjap0d 10443 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) # 0) | ||
Theorem | recjd 10444 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
Theorem | imcjd 10445 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
Theorem | cjmulrcld 10446 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
Theorem | cjmulvald 10447 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | cjmulge0d 10448 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
Theorem | renegd 10449 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
Theorem | imnegd 10450 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
Theorem | cjnegd 10451 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴)) | ||
Theorem | addcjd 10452 | 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 10453 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
Theorem | readdd 10454 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
Theorem | imaddd 10455 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
Theorem | resubd 10456 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
Theorem | imsubd 10457 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
Theorem | remuld 10458 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | immuld 10459 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
Theorem | cjaddd 10460 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) | ||
Theorem | cjmuld 10461 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) | ||
Theorem | ipcnd 10462 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
Theorem | cjdivapd 10463 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 # 0) ⇒ ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
Theorem | rered 10464 | 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 10465 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) = 0) | ||
Theorem | cjred 10466 | 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 10467 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
Theorem | immul2d 10468 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
Theorem | redivapd 10469 | Real part of a division. Related to remul2 10368. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴)) | ||
Theorem | imdivapd 10470 | Imaginary part of a division. Related to remul2 10368. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴)) | ||
Theorem | crred 10471 | 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 10472 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵) | ||
Theorem | caucvgrelemrec 10473* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (℩𝑟 ∈ ℝ (𝐴 · 𝑟) = 1) = (1 / 𝐴)) | ||
Theorem | caucvgrelemcau 10474* | Lemma for caucvgre 10475. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ ℕ (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) | ||
Theorem | caucvgre 10475* |
Convergence of real sequences.
A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (1 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (1 / 𝑛)))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) | ||
Theorem | cvg1nlemcxze 10476 | Lemma for cvg1n 10480. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ ℝ+) & ⊢ (𝜑 → 𝑍 ∈ ℕ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → ((((𝐶 · 2) / 𝑋) / 𝑍) + 𝐴) < 𝐸) ⇒ ⊢ (𝜑 → (𝐶 / (𝐸 · 𝑍)) < (𝑋 / 2)) | ||
Theorem | cvg1nlemf 10477* | Lemma for cvg1n 10480. The modified sequence 𝐺 is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) & ⊢ (𝜑 → 𝑍 ∈ ℕ) & ⊢ (𝜑 → 𝐶 < 𝑍) ⇒ ⊢ (𝜑 → 𝐺:ℕ⟶ℝ) | ||
Theorem | cvg1nlemcau 10478* | Lemma for cvg1n 10480. By selecting spaced out terms for the modified sequence 𝐺, the terms are within 1 / 𝑛 (without the constant 𝐶). (Contributed by Jim Kingdon, 1-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) & ⊢ (𝜑 → 𝑍 ∈ ℕ) & ⊢ (𝜑 → 𝐶 < 𝑍) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐺‘𝑛) < ((𝐺‘𝑘) + (1 / 𝑛)) ∧ (𝐺‘𝑘) < ((𝐺‘𝑛) + (1 / 𝑛)))) | ||
Theorem | cvg1nlemres 10479* | Lemma for cvg1n 10480. The original sequence 𝐹 has a limit (turns out it is the same as the limit of the modified sequence 𝐺). (Contributed by Jim Kingdon, 1-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) & ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍))) & ⊢ (𝜑 → 𝑍 ∈ ℕ) & ⊢ (𝜑 → 𝐶 < 𝑍) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) | ||
Theorem | cvg1n 10480* |
Convergence of real sequences.
This is a version of caucvgre 10475 with a constant multiplier 𝐶 on the rate of convergence. That is, all terms after the nth term must be within 𝐶 / 𝑛 of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑛) < ((𝐹‘𝑘) + (𝐶 / 𝑛)) ∧ (𝐹‘𝑘) < ((𝐹‘𝑛) + (𝐶 / 𝑛)))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹‘𝑖) + 𝑥))) | ||
Theorem | uzin2 10481 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥) | ||
Theorem | rexanuz 10482* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | rexfiuz 10483* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexuz3 10484* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexanuz2 10485* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | r19.29uz 10486* | A version of 19.29 1557 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | ||
Theorem | r19.2uz 10487* | A version of r19.2m 3373 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑) | ||
Theorem | recvguniqlem 10488 | Lemma for recvguniq 10489. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝐴 < ((𝐹‘𝐾) + ((𝐴 − 𝐵) / 2))) & ⊢ (𝜑 → (𝐹‘𝐾) < (𝐵 + ((𝐴 − 𝐵) / 2))) ⇒ ⊢ (𝜑 → ⊥) | ||
Theorem | recvguniq 10489* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) < (𝐿 + 𝑥) ∧ 𝐿 < ((𝐹‘𝑘) + 𝑥))) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) < (𝑀 + 𝑥) ∧ 𝑀 < ((𝐹‘𝑘) + 𝑥))) ⇒ ⊢ (𝜑 → 𝐿 = 𝑀) | ||
Syntax | csqrt 10490 | Extend class notation to include square root of a complex number. |
class √ | ||
Syntax | cabs 10491 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-rsqrt 10492* |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) |
⊢ √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦))) | ||
Definition | df-abs 10493 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) | ||
Theorem | sqrtrval 10494* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
⊢ (𝐴 ∈ ℝ → (√‘𝐴) = (℩𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))) | ||
Theorem | absval 10495 | 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 10496 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+) | ||
Theorem | sqrt0rlem 10497 | Lemma for sqrt0 10498. (Contributed by Jim Kingdon, 26-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ 𝐴)) ↔ 𝐴 = 0) | ||
Theorem | sqrt0 10498 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (√‘0) = 0 | ||
Theorem | resqrexlem1arp 10499 | Lemma for resqrex 10520. 1 + 𝐴 is a positive real (expressed in a way that will help apply seqf 9941 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((ℕ × {(1 + 𝐴)})‘𝑁) ∈ ℝ+) | ||
Theorem | resqrexlemp1rp 10500* | Lemma for resqrex 10520. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 9941 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝐶) ∈ ℝ+) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |