![]() |
Metamath
Proof Explorer Theorem List (p. 155 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | absge0i 15401 | Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (abs‘𝐴) | ||
Theorem | absval2i 15402 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | abs00i 15403 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((abs‘𝐴) = 0 ↔ 𝐴 = 0) | ||
Theorem | absgt0i 15404 | The absolute value of a nonzero number is positive. Remark in [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 ↔ 0 < (abs‘𝐴)) | ||
Theorem | absnegi 15405 | Absolute value of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘-𝐴) = (abs‘𝐴) | ||
Theorem | abscji 15406 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘(∗‘𝐴)) = (abs‘𝐴) | ||
Theorem | releabsi 15407 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (ℜ‘𝐴) ≤ (abs‘𝐴) | ||
Theorem | abssubi 15408 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴)) | ||
Theorem | absmuli 15409 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 1-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵)) | ||
Theorem | sqabsaddi 15410 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘(𝐴 + 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) + (2 · (ℜ‘(𝐴 · (∗‘𝐵))))) | ||
Theorem | sqabssubi 15411 | Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))) | ||
Theorem | absdivzi 15412 | Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | abstrii 15413 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. This is Metamath 100 proof #91. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵)) | ||
Theorem | abs3difi 15414 | Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))) | ||
Theorem | abs3lemi 15415 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷) | ||
Theorem | rpsqrtcld 15416 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℝ+) | ||
Theorem | sqrtgt0d 15417 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < (√‘𝐴)) | ||
Theorem | absnidd 15418 | A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = -𝐴) | ||
Theorem | leabsd 15419 | A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ (abs‘𝐴)) | ||
Theorem | absord 15420 | The absolute value of a real number is either that number or its negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) | ||
Theorem | absred 15421 | Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘𝐴) = (√‘(𝐴↑2))) | ||
Theorem | resqrtcld 15422 | The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℝ) | ||
Theorem | sqrtmsqd 15423 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrtsqd 15424 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqrtge0d 15425 | The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (√‘𝐴)) | ||
Theorem | sqrtnegd 15426 | The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘-𝐴) = (i · (√‘𝐴))) | ||
Theorem | absidd 15427 | A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 𝐴) | ||
Theorem | sqrtdivd 15428 | Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) | ||
Theorem | sqrtmuld 15429 | Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtsq2d 15430 | Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2))) | ||
Theorem | sqrtled 15431 | Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtltd 15432 | Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | sqr11d 15433 | The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → (√‘𝐴) = (√‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | absltd 15434 | Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absled 15435 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | abssubge0d 15436 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | ||
Theorem | abssuble0d 15437 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | absdifltd 15438 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifled 15439 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | icodiamlt 15440 | Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ (𝐴[,)𝐵) ∧ 𝐷 ∈ (𝐴[,)𝐵))) → (abs‘(𝐶 − 𝐷)) < (𝐵 − 𝐴)) | ||
Theorem | abscld 15441 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ) | ||
Theorem | sqrtcld 15442 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℂ) | ||
Theorem | sqrtrege0d 15443 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (ℜ‘(√‘𝐴))) | ||
Theorem | sqsqrtd 15444 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | msqsqrtd 15445 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
Theorem | sqr00d 15446 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (√‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | absvalsqd 15447 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) | ||
Theorem | absvalsq2d 15448 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | absge0d 15449 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (abs‘𝐴)) | ||
Theorem | absval2d 15450 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) | ||
Theorem | abs00d 15451 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (abs‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | absne0d 15452 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) ≠ 0) | ||
Theorem | absrpcld 15453 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+) | ||
Theorem | absnegd 15454 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘-𝐴) = (abs‘𝐴)) | ||
Theorem | abscjd 15455 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(∗‘𝐴)) = (abs‘𝐴)) | ||
Theorem | releabsd 15456 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (ℜ‘𝐴) ≤ (abs‘𝐴)) | ||
Theorem | absexpd 15457 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | abssubd 15458 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))) | ||
Theorem | absmuld 15459 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵))) | ||
Theorem | absdivd 15460 | Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | abstrid 15461 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difd 15462 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs2dif2d 15463 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difabsd 15464 | Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs3difd 15465 | Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) | ||
Theorem | abs3lemd 15466 | Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) & ⊢ (𝜑 → (abs‘(𝐴 − 𝐶)) < (𝐷 / 2)) & ⊢ (𝜑 → (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) < 𝐷) | ||
Theorem | reusq0 15467* | A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023.) |
⊢ (𝑋 ∈ ℂ → (∃!𝑥 ∈ ℂ (𝑥↑2) = 𝑋 ↔ 𝑋 = 0)) | ||
Theorem | bhmafibid1cn 15468 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid2cn 15469 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid1 15470 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn 15468, and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020.) (Proof modification is discouraged.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | ||
Theorem | bhmafibid2 15471 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | ||
Syntax | clsp 15472 | Extend class notation to include the limsup function. |
class lim sup | ||
Definition | df-limsup 15473* | Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 15476 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.) |
⊢ lim sup = (𝑥 ∈ V ↦ inf(ran (𝑘 ∈ ℝ ↦ sup(((𝑥 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )) | ||
Theorem | limsupgord 15474 | Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → sup(((𝐹 “ (𝐵[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝐴[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
Theorem | limsupcl 15475 | Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.) |
⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) ∈ ℝ*) | ||
Theorem | limsupval 15476* | The superior limit of an infinite sequence 𝐹 of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of 𝐹. Definition 12-4.1 of [Gleason] p. 175. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2014.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, < )) | ||
Theorem | limsupgf 15477* | Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ 𝐺:ℝ⟶ℝ* | ||
Theorem | limsupgval 15478* | Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (𝑀 ∈ ℝ → (𝐺‘𝑀) = sup(((𝐹 “ (𝑀[,)+∞)) ∩ ℝ*), ℝ*, < )) | ||
Theorem | limsupgle 15479* | The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*) → ((𝐺‘𝐶) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) | ||
Theorem | limsuple 15480* | The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 ≤ (lim sup‘𝐹) ↔ ∀𝑗 ∈ ℝ 𝐴 ≤ (𝐺‘𝑗))) | ||
Theorem | limsuplt 15481* | The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) ⇒ ⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ 𝐴 ∈ ℝ*) → ((lim sup‘𝐹) < 𝐴 ↔ ∃𝑗 ∈ ℝ (𝐺‘𝑗) < 𝐴)) | ||
Theorem | limsupval2 15482* | The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) = inf((𝐺 “ 𝐴), ℝ*, < )) | ||
Theorem | limsupgre 15483* | If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) & ⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ) | ||
Theorem | limsupbnd1 15484* | If a sequence is eventually at most 𝐴, then the limsup is also at most 𝐴. (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / 𝑛 which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)) ⇒ ⊢ (𝜑 → (lim sup‘𝐹) ≤ 𝐴) | ||
Theorem | limsupbnd2 15485* | If a sequence is eventually greater than 𝐴, then the limsup is also greater than 𝐴. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → sup(𝐵, ℝ*, < ) = +∞) & ⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗))) ⇒ ⊢ (𝜑 → 𝐴 ≤ (lim sup‘𝐹)) | ||
Syntax | cli 15486 | Extend class notation with convergence relation for limits. |
class ⇝ | ||
Syntax | crli 15487 | Extend class notation with real convergence relation for limits. |
class ⇝𝑟 | ||
Syntax | co1 15488 | Extend class notation with the set of all eventually bounded functions. |
class 𝑂(1) | ||
Syntax | clo1 15489 | Extend class notation with the set of all eventually upper bounded functions. |
class ≤𝑂(1) | ||
Definition | df-clim 15490* | Define the limit relation for complex number sequences. See clim 15496 for its relational expression. (Contributed by NM, 28-Aug-2005.) |
⊢ ⇝ = {〈𝑓, 𝑦〉 ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))} | ||
Definition | df-rlim 15491* | Define the limit relation for partial functions on the reals. See rlim 15497 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ ⇝𝑟 = {〈𝑓, 𝑥〉 ∣ ((𝑓 ∈ (ℂ ↑pm ℝ) ∧ 𝑥 ∈ ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ dom 𝑓(𝑧 ≤ 𝑤 → (abs‘((𝑓‘𝑤) − 𝑥)) < 𝑦))} | ||
Definition | df-o1 15492* | Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of 𝑂(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ 𝑂(1) = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(abs‘(𝑓‘𝑦)) ≤ 𝑚} | ||
Definition | df-lo1 15493* | Define the set of eventually upper bounded real functions. This fills a gap in 𝑂(1) coverage, to express statements like 𝑓(𝑥) ≤ 𝑔(𝑥) + 𝑂(𝑥) via (𝑥 ∈ ℝ+ ↦ (𝑓(𝑥) − 𝑔(𝑥)) / 𝑥) ∈ ≤𝑂(1). (Contributed by Mario Carneiro, 25-May-2016.) |
⊢ ≤𝑂(1) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ 𝑚} | ||
Theorem | climrel 15494 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ Rel ⇝ | ||
Theorem | rlimrel 15495 | The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.) |
⊢ Rel ⇝𝑟 | ||
Theorem | clim 15496* | Express the predicate: The limit of complex number sequence 𝐹 is 𝐴, or 𝐹 converges to 𝐴. This means that for any real 𝑥, no matter how small, there always exists an integer 𝑗 such that the absolute difference of any later complex number in the sequence and the limit is less than 𝑥. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝐹‘𝑘) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵 ∈ ℂ ∧ (abs‘(𝐵 − 𝐴)) < 𝑥)))) | ||
Theorem | rlim 15497* | Express the predicate: The limit of complex number function 𝐹 is 𝐶, or 𝐹 converges to 𝐶, in the real sense. This means that for any real 𝑥, no matter how small, there always exists a number 𝑦 such that the absolute difference of any number in the function beyond 𝑦 and the limit is less than 𝑥. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)))) | ||
Theorem | rlim2 15498* | Rewrite rlim 15497 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
Theorem | rlim2lt 15499* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 < 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) | ||
Theorem | rlim3 15500* | Restrict the range of the domain bound to reals greater than some 𝐷 ∈ ℝ. (Contributed by Mario Carneiro, 16-Sep-2014.) |
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ (𝐷[,)+∞)∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |