![]() |
Metamath
Proof Explorer Theorem List (p. 145 of 435) | < 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-28330) |
![]() (28331-29855) |
![]() (29856-43447) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | absval2 14401 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) | ||
Theorem | abs0 14402 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (abs‘0) = 0 | ||
Theorem | absi 14403 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (abs‘i) = 1 | ||
Theorem | absge0 14404 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴)) | ||
Theorem | absrpcl 14405 | 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 14406 | 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 14407 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 14406. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | abs00bd 14408 | If a complex number is zero, its absolute value is zero. Converse of abs00d 14562. One-way deduction form of abs00 14406. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 0) | ||
Theorem | absreimsq 14409 | 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 14410 | 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 14411 | 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 14412 | Absolute value distributes over division. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | absid 14413 | 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 14414 | The absolute value of one is one. (Contributed by David A. Wheeler, 16-Jul-2016.) |
⊢ (abs‘1) = 1 | ||
Theorem | absnid 14415 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴) | ||
Theorem | leabs 14416 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) | ||
Theorem | absor 14417 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) | ||
Theorem | absre 14418 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2))) | ||
Theorem | absresq 14419 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2)) | ||
Theorem | absmod0 14420 | 𝐴 is divisible by 𝐵 iff its absolute value is. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 mod 𝐵) = 0 ↔ ((abs‘𝐴) mod 𝐵) = 0)) | ||
Theorem | absexp 14421 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | absexpz 14422 | Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | abssq 14423 | 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 14424 | 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 14425 | 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 14426 | 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 14427 | 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 14428 | 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 14429 | 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 14430 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ) | ||
Theorem | abslt 14431 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absle 14432 | 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 14433 | 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 14434 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifle 14435 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | elicc4abs 14436 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵)) | ||
Theorem | lenegsq 14437 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | releabs 14438 | 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 14439 | Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2))) | ||
Theorem | absidm 14440 | The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004.) |
⊢ (𝐴 ∈ ℂ → (abs‘(abs‘𝐴)) = (abs‘𝐴)) | ||
Theorem | absgt0 14441 | 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 14442 | 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 14443 | 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 14444 | Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | ||
Theorem | abssuble0 14445 | Absolute value of a nonpositive difference. (Contributed by FL, 3-Jan-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) | ||
Theorem | absmax 14446 | The maximum of two numbers using absolute value. (Contributed by NM, 7-Aug-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → if(𝐴 ≤ 𝐵, 𝐵, 𝐴) = (((𝐴 + 𝐵) + (abs‘(𝐴 − 𝐵))) / 2)) | ||
Theorem | abstri 14447 | 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 14448 | Absolute value of differences around common element. (Contributed by FL, 9-Oct-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) | ||
Theorem | abs2dif 14449 | Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs2dif2 14450 | Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) | ||
Theorem | abs2difabs 14451 | Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))) | ||
Theorem | abs1m 14452* | 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 14453* | Cancellation law involving the real part of a complex number. (Contributed by NM, 12-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ (ℜ‘(𝑥 · 𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵)) | ||
Theorem | absf 14454 | 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 14455 | Lemma involving absolute value of differences. (Contributed by NM, 2-Oct-1999.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) → (((abs‘(𝐴 − 𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)) | ||
Theorem | abslem2 14456 | Lemma involving absolute values. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((∗‘(𝐴 / (abs‘𝐴))) · 𝐴) + ((𝐴 / (abs‘𝐴)) · (∗‘𝐴))) = (2 · (abs‘𝐴))) | ||
Theorem | rddif 14457 | 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 14458 | 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 14459 | Lemma for fzomaxdif 14460. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶))) | ||
Theorem | fzomaxdif 14460 | 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 14461 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐴 ∈ ran ℤ≥ ∧ 𝐵 ∈ ran ℤ≥) → (𝐴 ∩ 𝐵) ∈ ran ℤ≥) | ||
Theorem | rexanuz 14462* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
⊢ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | rexanre 14463* | Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.) |
⊢ (𝐴 ⊆ ℝ → (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → (𝜑 ∧ 𝜓)) ↔ (∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ∧ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜓)))) | ||
Theorem | rexfiuz 14464* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐴 𝜑 ↔ ∀𝑛 ∈ 𝐴 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexuz3 14465* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) | ||
Theorem | rexanuz2 14466* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) | ||
Theorem | r19.29uz 14467* | A version of 19.29 1978 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((∀𝑘 ∈ 𝑍 𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | ||
Theorem | r19.2uz 14468* | A version of r19.2z 4282 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∃𝑘 ∈ 𝑍 𝜑) | ||
Theorem | rexuzre 14469* | Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝑍 (𝑗 ≤ 𝑘 → 𝜑))) | ||
Theorem | rexico 14470* | Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑗 ∈ (𝐵[,)+∞)∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑) ↔ ∃𝑗 ∈ ℝ ∀𝑘 ∈ 𝐴 (𝑗 ≤ 𝑘 → 𝜑))) | ||
Theorem | cau3lem 14471* | Lemma for cau3 14472. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝑍 ⊆ ℤ & ⊢ (𝜏 → 𝜓) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒)) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗)))) & ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) | ||
Theorem | cau3 14472* | 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 14462 and friends.) (Contributed by Mario Carneiro, 15-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(abs‘((𝐹‘𝑘) − (𝐹‘𝑚))) < 𝑥)) | ||
Theorem | cau4 14473* | Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑊 = (ℤ≥‘𝑁) ⇒ ⊢ (𝑁 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑊 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) | ||
Theorem | caubnd2 14474* | A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑦) | ||
Theorem | caubnd 14475* | 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 14476 | Lemma for sqreu 14477: 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 14477* | Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)) | ||
Theorem | sqrtcl 14478 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (√‘𝐴) ∈ ℂ) | ||
Theorem | sqrtthlem 14479 | Lemma for sqrtth 14481. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+)) | ||
Theorem | sqrtf 14480 | Mapping domain and codomain of the square root function. (Contributed by Mario Carneiro, 13-Sep-2015.) |
⊢ √:ℂ⟶ℂ | ||
Theorem | sqrtth 14481 | Square root theorem over the complex numbers. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtrege0 14482 | 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 14483 | Solve an equation containing a square. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = 𝐵 ↔ (𝐴 = (√‘𝐵) ∨ 𝐴 = -(√‘𝐵)))) | ||
Theorem | eqsqrtd 14484 | 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 14485 | A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 𝐵) & ⊢ (𝜑 → 0 < (ℜ‘𝐴)) ⇒ ⊢ (𝜑 → 𝐴 = (√‘𝐵)) | ||
Theorem | amgm2 14486 | 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 14487 | 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 14488 | 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 14489 | 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 14490 | Square root of square. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrtsqi 14491 | Square root of square. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqsqrti 14492 | Square of square root. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | sqrtge0i 14493 | 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 14494 | A nonnegative number is its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (0 ≤ 𝐴 → (abs‘𝐴) = 𝐴) | ||
Theorem | absnidi 14495 | A negative number is the negative of its own absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≤ 0 → (abs‘𝐴) = -𝐴) | ||
Theorem | leabsi 14496 | A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ≤ (abs‘𝐴) | ||
Theorem | absori 14497 | The absolute value of a real number is either that number or its negative. (Contributed by NM, 30-Sep-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴) | ||
Theorem | absrei 14498 | Absolute value of a real number. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (abs‘𝐴) = (√‘(𝐴↑2)) | ||
Theorem | sqrtpclii 14499 | The square root of a positive real is a real. (Contributed by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ (√‘𝐴) ∈ ℝ | ||
Theorem | sqrtgt0ii 14500 | The square root of a positive real is positive. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 6-Sep-2013.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 0 < (√‘𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |