| Metamath
Proof Explorer Theorem List (p. 153 of 493) | < 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-30927) |
(30928-32450) |
(32451-49297) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sqeqd 15201 | 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 15202 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ∈ ℝ | ||
| Theorem | imcli 15203 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘𝐴) ∈ ℝ | ||
| Theorem | cjcli 15204 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘𝐴) ∈ ℂ | ||
| Theorem | replimi 15205 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))) | ||
| Theorem | cjcji 15206 | 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 15207 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℑ‘𝐴) = 0) | ||
| Theorem | rerebi 15208 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ∈ ℝ ↔ (ℜ‘𝐴) = 𝐴) | ||
| Theorem | cjrebi 15209 | 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 15210 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴) | ||
| Theorem | imcji 15211 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴) | ||
| Theorem | cjmulrcli 15212 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) ∈ ℝ | ||
| Theorem | cjmulvali 15213 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
| Theorem | cjmulge0i 15214 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (𝐴 · (∗‘𝐴)) | ||
| Theorem | renegi 15215 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘-𝐴) = -(ℜ‘𝐴) | ||
| Theorem | imnegi 15216 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℑ‘-𝐴) = -(ℑ‘𝐴) | ||
| Theorem | cjnegi 15217 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (∗‘-𝐴) = -(∗‘𝐴) | ||
| Theorem | addcji 15218 | 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 15219 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)) | ||
| Theorem | imaddi 15220 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)) | ||
| Theorem | remuli 15221 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
| Theorem | immuli 15222 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))) | ||
| Theorem | cjaddi 15223 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)) | ||
| Theorem | cjmuli 15224 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)) | ||
| Theorem | ipcni 15225 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))) | ||
| Theorem | cjdivi 15226 | Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
| Theorem | crrei 15227 | 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 15228 | 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 15229 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ∈ ℝ) | ||
| Theorem | imcld 15230 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) | ||
| Theorem | cjcld 15231 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘𝐴) ∈ ℂ) | ||
| Theorem | replimd 15232 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴)))) | ||
| Theorem | remimd 15233 | 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 15234 | 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 15235 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (ℑ‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
| Theorem | rerebd 15236 | 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 15237 | 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 15238 | A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘𝐴) ≠ 0) | ||
| Theorem | recjd 15239 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴)) | ||
| Theorem | imcjd 15240 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴)) | ||
| Theorem | cjmulrcld 15241 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ) | ||
| Theorem | cjmulvald 15242 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
| Theorem | cjmulge0d 15243 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴))) | ||
| Theorem | renegd 15244 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴)) | ||
| Theorem | imnegd 15245 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴)) | ||
| Theorem | cjnegd 15246 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘-𝐴) = -(∗‘𝐴)) | ||
| Theorem | addcjd 15247 | 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 15248 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (∗‘(𝐴↑𝑁)) = ((∗‘𝐴)↑𝑁)) | ||
| Theorem | readdd 15249 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) | ||
| Theorem | imaddd 15250 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) | ||
| Theorem | resubd 15251 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 − 𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵))) | ||
| Theorem | imsubd 15252 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 − 𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵))) | ||
| Theorem | remuld 15253 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
| Theorem | immuld 15254 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))) | ||
| Theorem | cjaddd 15255 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) | ||
| Theorem | cjmuld 15256 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))) | ||
| Theorem | ipcnd 15257 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))) | ||
| Theorem | cjdivd 15258 | Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵))) | ||
| Theorem | rered 15259 | 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 15260 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (ℑ‘𝐴) = 0) | ||
| Theorem | cjred 15261 | 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 15262 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵))) | ||
| Theorem | immul2d 15263 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵))) | ||
| Theorem | redivd 15264 | Real part of a division. Related to remul2 15165. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴)) | ||
| Theorem | imdivd 15265 | Imaginary part of a division. Related to remul2 15165. (Contributed by Mario Carneiro, 29-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴)) | ||
| Theorem | crred 15266 | 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 15267 | 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 15268 | Extend class notation to include square root of a complex number. |
| class √ | ||
| Syntax | cabs 15269 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
| class abs | ||
| Definition | df-sqrt 15270* |
Define a function whose value is the square root of a complex number.
For example, (√‘25) = 5 (ex-sqrt 30463).
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 30463. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 15396 for its closure, sqrtval 15272 for its value, sqrtth 15399 and sqsqrti 15410 for its relationship to squares, and sqrt11i 15419 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.) |
| ⊢ √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))) | ||
| Definition | df-abs 15271 | Define the function for the absolute value (modulus) of a complex number. See abscli 15430 for its closure and absval 15273 or absval2i 15432 for its value. For example, (abs‘-2) = 2 (ex-abs 30464). (Contributed by NM, 27-Jul-1999.) |
| ⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) | ||
| Theorem | sqrtval 15272* | Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.) |
| ⊢ (𝐴 ∈ ℂ → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))) | ||
| Theorem | absval 15273 | 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 15274 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
| ⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+) | ||
| Theorem | cnpart 15275 | 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 | sqrt0 15276 | The square root of zero is zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ (√‘0) = 0 | ||
| Theorem | 01sqrexlem1 15277* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1) | ||
| Theorem | 01sqrexlem2 15278* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆) | ||
| Theorem | 01sqrexlem3 15279* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧)) | ||
| Theorem | 01sqrexlem4 15280* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) | ||
| Theorem | 01sqrexlem5 15281* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < ))) | ||
| Theorem | 01sqrexlem6 15282* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴) | ||
| Theorem | 01sqrexlem7 15283* | Lemma for 01sqrex 15284. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
| ⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴) | ||
| Theorem | 01sqrex 15284* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴)) | ||
| Theorem | resqrex 15285* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴)) | ||
| Theorem | sqrmo 15286* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
| ⊢ (𝐴 ∈ ℂ → ∃*𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
| Theorem | resqreu 15287* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
| Theorem | resqrtcl 15288 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ) | ||
| Theorem | resqrtthlem 15289 | Lemma for resqrtth 15290. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+)) | ||
| Theorem | resqrtth 15290 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴) | ||
| Theorem | remsqsqrt 15291 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
| Theorem | sqrtge0 15292 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (√‘𝐴)) | ||
| Theorem | sqrtgt0 15293 | The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (√‘𝐴)) | ||
| Theorem | sqrtmul 15294 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
| Theorem | sqrtle 15295 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
| Theorem | sqrtlt 15296 | Square root is strictly monotonic. Closed form of sqrtlti 15424. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
| Theorem | sqrt11 15297 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | sqrt00 15298 | A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
| Theorem | rpsqrtcl 15299 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
| ⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+) | ||
| Theorem | sqrtdiv 15300 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |