Home | Metamath
Proof Explorer Theorem List (p. 150 of 463) | < 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-29023) |
Hilbert Space Explorer
(29024-30546) |
Users' Mathboxes
(30547-46208) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zabscl 14901 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ) | ||
Theorem | abslt 14902 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absle 14903 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) | ||
Theorem | abssubne0 14904 | If the absolute value of a complex number is less than a real, its difference from the real is nonzero. (Contributed by NM, 2-Nov-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ (abs‘𝐴) < 𝐵) → (𝐵 − 𝐴) ≠ 0) | ||
Theorem | absdiflt 14905 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifle 14906 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | elicc4abs 14907 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵)) | ||
Theorem | lenegsq 14908 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | releabs 14909 | 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, 1-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ≤ (abs‘𝐴)) | ||
Theorem | recval 14910 | Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2))) | ||
Theorem | absidm 14911 | The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.) |
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴)) | ||
Theorem | absgt0 14912 | The absolute value of a nonzero number is positive. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ 0 < (abs‘𝐴))) | ||
Theorem | nnabscl 14913 | The absolute value of a nonzero integer is a positive integer. (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈ ℕ) | ||
Theorem | abssub 14914 | Swapping order of subtraction doesn't change the absolute value. (Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))) | ||
Theorem | abssubge0 14915 | Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | ||
Theorem | abssuble0 14916 | Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | absmax 14917 | The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) | ||
Theorem | abstri 14918 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by NM, 7-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs3dif 14919 | Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) | ||
Theorem | abs2dif 14920 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs2dif2 14921 | Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difabs 14922 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs1m 14923* | For any complex number, there exists a unit-magnitude multiplier that produces its absolute value. Part of proof of Theorem 13-2.12 of [Gleason] p. 195. (Contributed by NM, 26-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ ((abs‘𝑥) = 1 ∧ (abs‘𝐴) = (𝑥 · 𝐴))) | ||
Theorem | recan 14924* | Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ (ℜ‘(𝑥 · 𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | absf 14925 | Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) |
⊢ abs:ℂ⟶ℝ | ||
Theorem | abs3lem 14926 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)) | ||
Theorem | abslem2 14927 | Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((∗‘(𝐴 / (abs‘𝐴))) · 𝐴) + ((𝐴 / (abs‘𝐴)) · (∗‘𝐴))) = (2 · (abs‘𝐴))) | ||
Theorem | rddif 14928 | The difference between a real number and its nearest integer is less than or equal to one half. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝐴 ∈ ℝ → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ≤ (1 / 2)) | ||
Theorem | absrdbnd 14929 | Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Sep-2015.) |
⊢ (𝐴 ∈ ℝ → (abs‘(⌊‘(𝐴 + (1 / 2)))) ≤ ((⌊‘(abs‘𝐴)) + 1)) | ||
Theorem | fzomaxdiflem 14930 | Lemma for fzomaxdif 14931. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶))) | ||
Theorem | fzomaxdif 14931 | A bound on the separation of two points in a half-open range. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (abs‘(𝐴 − 𝐵)) ∈ (0..^(𝐷 − 𝐶))) | ||
Theorem | uzin2 14932 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥) | ||
Theorem | rexanuz 14933* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | rexanre 14934* | Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.) |
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓)))) | ||
Theorem | rexfiuz 14935* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexuz3 14936* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexanuz2 14937* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | r19.29uz 14938* | A version of 19.29 1881 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | ||
Theorem | r19.2uz 14939* | A version of r19.2z 4420 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑) | ||
Theorem | rexuzre 14940* | Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑))) | ||
Theorem | rexico 14941* | Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) | ||
Theorem | cau3lem 14942* | Lemma for cau3 14943. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝑍 ⊆ ℤ & ⊢ (𝜏 → 𝜓) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒)) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗)))) & ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) | ||
Theorem | cau3 14943* | 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 14933 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)) | ||
Theorem | cau4 14944* | Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) ⇒ ⊢ (𝑁 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | ||
Theorem | caubnd2 14945* | A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑦) | ||
Theorem | caubnd 14946* | 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 14947 | Lemma for sqreu 14948: 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 14948* | Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | sqrtcl 14949 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ) | ||
Theorem | sqrtthlem 14950 | Lemma for sqrtth 14952. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+)) | ||
Theorem | sqrtf 14951 | Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ √:ℂ⟶ℂ | ||
Theorem | sqrtth 14952 | Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtrege0 14953 | 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 14954 | Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = 𝐵 ↔ (𝐴 = (√‘𝐵) ∨ 𝐴 = -(√‘𝐵)))) | ||
Theorem | eqsqrtd 14955 | 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 14956 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 𝐵) & ⊢ (𝜑 → 0 < (ℜ‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 = (√‘𝐵)) | ||
Theorem | amgm2 14957 | 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 14958 | 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 14959 | 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 14960 | 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 14961 | Square root of square. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrtsqi 14962 | Square root of square. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqsqrti 14963 | Square of square root. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtge0i 14964 | 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 14965 | A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (abs‘𝐴) = 𝐴) | ||
Theorem | absnidi 14966 | A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 0 → (abs‘𝐴) = -𝐴) | ||
Theorem | leabsi 14967 | A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ≤ (abs‘𝐴) | ||
Theorem | absori 14968 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴) | ||
Theorem | absrei 14969 | Absolute value of a real number. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (abs‘𝐴) = (√‘(𝐴↑2)) | ||
Theorem | sqrtpclii 14970 | The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ (√‘𝐴) ∈ ℝ | ||
Theorem | sqrtgt0ii 14971 | 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 14972 | The square root function is one-to-one. (Contributed by NM, 27-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sqrtmuli 14973 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtmulii 14974 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 ≤ 𝐴 & ⊢ 0 ≤ 𝐵 ⇒ ⊢ (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)) | ||
Theorem | sqrtmsq2i 14975 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐵))) | ||
Theorem | sqrtlei 14976 | Square root is monotonic. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtlti 14977 | Square root is strictly monotonic. (Contributed by Roy F. Longton, 8-Aug-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | abslti 14978 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵)) | ||
Theorem | abslei 14979 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) | ||
Theorem | cnsqrt00 14980 | A square root of a complex number is zero iff its argument is 0. Version of sqrt00 14851 for complex numbers. (Contributed by AV, 26-Jan-2023.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | absvalsqi 14981 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)) | ||
Theorem | absvalsq2i 14982 | Square of value of absolute value function. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) | ||
Theorem | abscli 14983 | Real closure of absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘𝐴) ∈ ℝ | ||
Theorem | absge0i 14984 | Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ 0 ≤ (abs‘𝐴) | ||
Theorem | absval2i 14985 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | abs00i 14986 | 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 14987 | 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 14988 | Absolute value of negative. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (abs‘-𝐴) = (abs‘𝐴) | ||
Theorem | abscji 14989 | 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 14990 | 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 14991 | 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 14992 | 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 14993 | 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 14994 | Square of absolute value of difference. (Contributed by Steve Rodriguez, 20-Jan-2007.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))) | ||
Theorem | absdivzi 14995 | Absolute value distributes over division. (Contributed by NM, 26-Mar-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐵 ≠ 0 → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | abstrii 14996 | 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 14997 | Absolute value of differences around common element. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵))) | ||
Theorem | abs3lemi 14998 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℝ ⇒ ⊢ (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷) | ||
Theorem | rpsqrtcld 14999 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (√‘𝐴) ∈ ℝ+) | ||
Theorem | sqrtgt0d 15000 | The square root of a positive real is positive. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < (√‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |