Home | Metamath
Proof Explorer Theorem List (p. 147 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqrlem1 14601* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∀𝑦 ∈ 𝑆 𝑦 ≤ 1) | ||
Theorem | sqrlem2 14602* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → 𝐴 ∈ 𝑆) | ||
Theorem | sqrlem3 14603* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧)) | ||
Theorem | sqrlem4 14604* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) | ||
Theorem | sqrlem5 14605* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < ))) | ||
Theorem | sqrlem6 14606* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) ≤ 𝐴) | ||
Theorem | sqrlem7 14607* | Lemma for 01sqrex 14608. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} & ⊢ 𝐵 = sup(𝑆, ℝ, < ) & ⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} ⇒ ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → (𝐵↑2) = 𝐴) | ||
Theorem | 01sqrex 14608* | Existence of a square root for reals in the interval (0, 1]. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1) → ∃𝑥 ∈ ℝ+ (𝑥 ≤ 1 ∧ (𝑥↑2) = 𝐴)) | ||
Theorem | resqrex 14609* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴)) | ||
Theorem | sqrmo 14610* | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
⊢ (𝐴 ∈ ℂ → ∃*𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | resqreu 14611* | Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | resqrtcl 14612 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ) | ||
Theorem | resqrtthlem 14613 | Lemma for resqrtth 14614. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+)) | ||
Theorem | resqrtth 14614 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | remsqsqrt 14615 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
Theorem | sqrtge0 14616 | 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 14617 | 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 14618 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtle 14619 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtlt 14620 | Square root is strictly monotonic. Closed form of sqrtlti 14748. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | sqrt11 14621 | The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sqrt00 14622 | 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 14623 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+) | ||
Theorem | sqrtdiv 14624 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) | ||
Theorem | sqrtneglem 14625 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((i · (√‘𝐴))↑2) = -𝐴 ∧ 0 ≤ (ℜ‘(i · (√‘𝐴))) ∧ (i · (i · (√‘𝐴))) ∉ ℝ+)) | ||
Theorem | sqrtneg 14626 | The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘-𝐴) = (i · (√‘𝐴))) | ||
Theorem | sqrtsq2 14627 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2))) | ||
Theorem | sqrtsq 14628 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqrtmsq 14629 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrt1 14630 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
⊢ (√‘1) = 1 | ||
Theorem | sqrt4 14631 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
⊢ (√‘4) = 2 | ||
Theorem | sqrt9 14632 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
⊢ (√‘9) = 3 | ||
Theorem | sqrt2gt1lt2 14633 | The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ (1 < (√‘2) ∧ (√‘2) < 2) | ||
Theorem | sqrtm1 14634 | The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of i, but the definition of √ df-sqrt 14593 has already been crafted with i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 10604 or i2 13564 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ i = (√‘-1) | ||
Theorem | nn0sqeq1 14635 | A natural number with square one is equal to one. (Contributed by Thierry Arnoux, 2-Feb-2020.) (Proof shortened by Thierry Arnoux, 6-Jun-2023.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁↑2) = 1) → 𝑁 = 1) | ||
Theorem | absneg 14636 | Absolute value of the opposite. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴)) | ||
Theorem | abscl 14637 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ) | ||
Theorem | abscj 14638 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘(∗‘𝐴)) = (abs‘𝐴)) | ||
Theorem | absvalsq 14639 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) | ||
Theorem | absvalsq2 14640 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | sqabsadd 14641 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 + 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) + (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))) | ||
Theorem | sqabssub 14642 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))) | ||
Theorem | absval2 14643 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) | ||
Theorem | abs0 14644 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (abs‘0) = 0 | ||
Theorem | absi 14645 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (abs‘i) = 1 | ||
Theorem | absge0 14646 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴)) | ||
Theorem | absrpcl 14647 | The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈ ℝ+) | ||
Theorem | abs00 14648 | 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, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | abs00ad 14649 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 14648. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | abs00bd 14650 | If a complex number is zero, its absolute value is zero. Converse of abs00d 14805. One-way deduction form of abs00 14648. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 0) | ||
Theorem | absreimsq 14651 | Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2))) | ||
Theorem | absreim 14652 | Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴 + (i · 𝐵))) = (√‘((𝐴↑2) + (𝐵↑2)))) | ||
Theorem | absmul 14653 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 · 𝐵)) = ((abs‘𝐴) · (abs‘𝐵))) | ||
Theorem | absdiv 14654 | Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | absid 14655 | A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴) | ||
Theorem | abs1 14656 | The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.) |
⊢ (abs‘1) = 1 | ||
Theorem | absnid 14657 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴) | ||
Theorem | leabs 14658 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) | ||
Theorem | absor 14659 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) | ||
Theorem | absre 14660 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2))) | ||
Theorem | absresq 14661 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2)) | ||
Theorem | absmod0 14662 | 𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0)) | ||
Theorem | absexp 14663 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | absexpz 14664 | Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | abssq 14665 | Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (abs‘(𝐴↑2))) | ||
Theorem | sqabs 14666 | The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴↑2) = (𝐵↑2) ↔ (abs‘𝐴) = (abs‘𝐵))) | ||
Theorem | absrele 14667 | The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘(ℜ‘𝐴)) ≤ (abs‘𝐴)) | ||
Theorem | absimle 14668 | The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) ≤ (abs‘𝐴)) | ||
Theorem | max0add 14669 | The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Mario Carneiro, 24-Aug-2014.) |
⊢ (𝐴 ∈ ℝ → (if(0 ≤ 𝐴, 𝐴, 0) + if(0 ≤ -𝐴, -𝐴, 0)) = (abs‘𝐴)) | ||
Theorem | absz 14670 | A real number is an integer iff its absolute value is an integer. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℤ ↔ (abs‘𝐴) ∈ ℤ)) | ||
Theorem | nn0abscl 14671 | The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0) | ||
Theorem | zabscl 14672 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ) | ||
Theorem | abslt 14673 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absle 14674 | 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 14675 | 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 14676 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifle 14677 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | elicc4abs 14678 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵)) | ||
Theorem | lenegsq 14679 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | releabs 14680 | 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 14681 | Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2))) | ||
Theorem | absidm 14682 | The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.) |
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴)) | ||
Theorem | absgt0 14683 | 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 14684 | 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 14685 | 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 14686 | Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | ||
Theorem | abssuble0 14687 | Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | absmax 14688 | The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) | ||
Theorem | abstri 14689 | 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 14690 | Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) | ||
Theorem | abs2dif 14691 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs2dif2 14692 | Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difabs 14693 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs1m 14694* | 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 14695* | Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ (ℜ‘(𝑥 · 𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | absf 14696 | 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 14697 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)) | ||
Theorem | abslem2 14698 | Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((∗‘(𝐴 / (abs‘𝐴))) · 𝐴) + ((𝐴 / (abs‘𝐴)) · (∗‘𝐴))) = (2 · (abs‘𝐴))) | ||
Theorem | rddif 14699 | 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 14700 | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |