Home | Metamath
Proof Explorer Theorem List (p. 148 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rexico 14701* | Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) | ||
Theorem | cau3lem 14702* | Lemma for cau3 14703. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝑍 ⊆ ℤ & ⊢ (𝜏 → 𝜓) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒)) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗)))) & ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) | ||
Theorem | cau3 14703* | Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of 𝑗 in the assertion, so it can be used with rexanuz 14693 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)) | ||
Theorem | cau4 14704* | Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) ⇒ ⊢ (𝑁 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | ||
Theorem | caubnd2 14705* | A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑦) | ||
Theorem | caubnd 14706* | A Cauchy sequence of complex numbers is bounded. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 14-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) | ||
Theorem | sqreulem 14707 | Lemma for sqreu 14708: write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ 𝐵 = ((√‘(abs‘𝐴)) · (((abs‘𝐴) + 𝐴) / (abs‘((abs‘𝐴) + 𝐴)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ ((abs‘𝐴) + 𝐴) ≠ 0) → ((𝐵↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝐵) ∧ (i · 𝐵) ∉ ℝ+)) | ||
Theorem | sqreu 14708* | Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | sqrtcl 14709 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ) | ||
Theorem | sqrtthlem 14710 | Lemma for sqrtth 14712. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+)) | ||
Theorem | sqrtf 14711 | Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ √:ℂ⟶ℂ | ||
Theorem | sqrtth 14712 | Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtrege0 14713 | The square root function must make a choice between the two roots, which differ by a sign change. In the general complex case, the choice of "positive" and "negative" is not so clear. The convention we use is to take the root with positive real part, unless 𝐴 is a nonpositive real (in which case both roots have 0 real part); in this case we take the one in the positive imaginary direction. Another way to look at this is that we choose the root that is largest with respect to lexicographic order on the complex numbers (sorting by real part first, then by imaginary part as tie-breaker). (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘(√‘𝐴))) | ||
Theorem | eqsqrtor 14714 | Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = 𝐵 ↔ (𝐴 = (√‘𝐵) ∨ 𝐴 = -(√‘𝐵)))) | ||
Theorem | eqsqrtd 14715 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 𝐵) & ⊢ (𝜑 → 0 ≤ (ℜ‘𝐴)) & ⊢ (𝜑 → ¬ (i · 𝐴) ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 = (√‘𝐵)) | ||
Theorem | eqsqrt2d 14716 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 𝐵) & ⊢ (𝜑 → 0 < (ℜ‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 = (√‘𝐵)) | ||
Theorem | amgm2 14717 | Arithmetic-geometric mean inequality for 𝑛 = 2. (Contributed by Mario Carneiro, 2-Jul-2014.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) ≤ ((𝐴 + 𝐵) / 2)) | ||
Theorem | sqrtthi 14718 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
Theorem | sqrtcli 14719 | The square root of a nonnegative real is a real. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘𝐴) ∈ ℝ) | ||
Theorem | sqrtgt0i 14720 | The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 < 𝐴 → 0 < (√‘𝐴)) | ||
Theorem | sqrtmsqi 14721 | Square root of square. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrtsqi 14722 | Square root of square. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqsqrti 14723 | Square of square root. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtge0i 14724 | The square root of a nonnegative real is nonnegative. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → 0 ≤ (√‘𝐴)) | ||
Theorem | absidi 14725 | A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (abs‘𝐴) = 𝐴) | ||
Theorem | absnidi 14726 | A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 0 → (abs‘𝐴) = -𝐴) | ||
Theorem | leabsi 14727 | A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ≤ (abs‘𝐴) | ||
Theorem | absori 14728 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴) | ||
Theorem | absrei 14729 | Absolute value of a real number. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (abs‘𝐴) = (√‘(𝐴↑2)) | ||
Theorem | sqrtpclii 14730 | The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ (√‘𝐴) ∈ ℝ | ||
Theorem | sqrtgt0ii 14731 | The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 0 < (√‘𝐴) | ||
Theorem | sqrt11i 14732 | The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sqrtmuli 14733 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtmulii 14734 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 ≤ 𝐴 & ⊢ 0 ≤ 𝐵 ⇒ ⊢ (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)) | ||
Theorem | sqrtmsq2i 14735 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐵))) | ||
Theorem | sqrtlei 14736 | Square root is monotonic. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtlti 14737 | Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | abslti 14738 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)) | ||
Theorem | abslei 14739 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) | ||
Theorem | cnsqrt00 14740 | A square root of a complex number is zero iff its argument is 0. Version of sqrt00 14611 for complex numbers. (Contributed by AV, 26-Jan-2023.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | absvalsqi 14741 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)) | ||
Theorem | absvalsq2i 14742 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | abscli 14743 | Real closure of absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘𝐴) ∈ ℝ | ||
Theorem | absge0i 14744 | Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (abs‘𝐴) | ||
Theorem | absval2i 14745 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | abs00i 14746 | 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 14747 | 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 14748 | Absolute value of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘-𝐴) = (abs‘𝐴) | ||
Theorem | abscji 14749 | 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 14750 | 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 14751 | 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 14752 | 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 14753 | 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 14754 | Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))) | ||
Theorem | absdivzi 14755 | Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | abstrii 14756 | 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 14757 | Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))) | ||
Theorem | abs3lemi 14758 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷) | ||
Theorem | rpsqrtcld 14759 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℝ+) | ||
Theorem | sqrtgt0d 14760 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < (√‘𝐴)) | ||
Theorem | absnidd 14761 | A negative number is the negative of its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = -𝐴) | ||
Theorem | leabsd 14762 | A real number is less than or equal to its absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≤ (abs‘𝐴)) | ||
Theorem | absord 14763 | 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 14764 | Absolute value of a real number. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (abs‘𝐴) = (√‘(𝐴↑2))) | ||
Theorem | resqrtcld 14765 | The square root of a nonnegative real is a real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℝ) | ||
Theorem | sqrtmsqd 14766 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrtsqd 14767 | Square root of square. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqrtge0d 14768 | The square root of a nonnegative real is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (√‘𝐴)) | ||
Theorem | sqrtnegd 14769 | The square root of a negative number. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (√‘-𝐴) = (i · (√‘𝐴))) | ||
Theorem | absidd 14770 | A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 𝐴) | ||
Theorem | sqrtdivd 14771 | Square root distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) | ||
Theorem | sqrtmuld 14772 | Square root distributes over multiplication. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtsq2d 14773 | Relationship between square root and squares. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2))) | ||
Theorem | sqrtled 14774 | Square root is monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtltd 14775 | Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | sqr11d 14776 | The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → (√‘𝐴) = (√‘𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | absltd 14777 | Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absled 14778 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | abssubge0d 14779 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | ||
Theorem | abssuble0d 14780 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | absdifltd 14781 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifled 14782 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | icodiamlt 14783 | 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 14784 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ) | ||
Theorem | sqrtcld 14785 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℂ) | ||
Theorem | sqrtrege0d 14786 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (ℜ‘(√‘𝐴))) | ||
Theorem | sqsqrtd 14787 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | msqsqrtd 14788 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
Theorem | sqr00d 14789 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (√‘𝐴) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | absvalsqd 14790 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) | ||
Theorem | absvalsq2d 14791 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | absge0d 14792 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → 0 ≤ (abs‘𝐴)) | ||
Theorem | absval2d 14793 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) | ||
Theorem | abs00d 14794 | 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 14795 | 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 14796 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ+) | ||
Theorem | absnegd 14797 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (abs‘-𝐴) = (abs‘𝐴)) | ||
Theorem | abscjd 14798 | 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 14799 | 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 14800 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |