![]() |
Metamath
Proof Explorer Theorem List (p. 258 of 443) | < 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-28474) |
![]() (28475-29999) |
![]() (30000-44279) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2sqlem6 25701* | Lemma for 2sq 25708. If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐵 → 𝑝 ∈ 𝑆)) & ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑆) | ||
Theorem | 2sqlem7 25702* | Lemma for 2sq 25708. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) | ||
Theorem | 2sqlem8a 25703* | Lemma for 2sqlem8 25704. (Contributed by Mario Carneiro, 4-Jun-2016.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) & ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) & ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ) | ||
Theorem | 2sqlem8 25704* | Lemma for 2sq 25708. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) & ⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) & ⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷)) & ⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷)) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
Theorem | 2sqlem9 25705* | Lemma for 2sq 25708. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} & ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ 𝑌) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑆) | ||
Theorem | 2sqlem10 25706* | Lemma for 2sq 25708. Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ ℕ ∧ 𝐵 ∥ 𝐴) → 𝐵 ∈ 𝑆) | ||
Theorem | 2sqlem11 25707* | Lemma for 2sq 25708. (Contributed by Mario Carneiro, 19-Jun-2015.) |
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) & ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆) | ||
Theorem | 2sq 25708* | All primes of the form 4𝑘 + 1 are sums of two squares. This is Metamath 100 proof #20. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
Theorem | 2sqblem 25709 | Lemma for 2sqb 25710. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2)) & ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) & ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2))) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵))) ⇒ ⊢ (𝜑 → (𝑃 mod 4) = 1) | ||
Theorem | 2sqb 25710* | The converse to 2sq 25708. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1))) | ||
Theorem | 2sq2 25711 | 2 is the sum of squares of two nonnegative integers iff the two integers are 1. (Contributed by AV, 19-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = 2 ↔ (𝐴 = 1 ∧ 𝐵 = 1))) | ||
Theorem | 2sqn0 25712 | If the sum of two squares is prime, none of the original number is zero. (Contributed by Thierry Arnoux, 4-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | 2sqcoprm 25713 | If the sum of two squares is prime, the two original numbers are coprime. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | ||
Theorem | 2sqmod 25714 | Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝐵 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝐶 ≤ 𝐷) & ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) & ⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | 2sqmo 25715* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 25710 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqnn0 25716* | All primes of the form 4𝑘 + 1 are sums of squares of two nonnegative integers. (Contributed by AV, 3-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ0 ∃𝑦 ∈ ℕ0 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
Theorem | 2sqnn 25717* | All primes of the form 4𝑘 + 1 are sums of squares of two positive integers. (Contributed by AV, 11-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑃 = ((𝑥↑2) + (𝑦↑2))) | ||
Theorem | addsq2reu 25718* |
For each complex number 𝐶, there exists a unique complex
number
𝑎 added to the square of a unique
another complex number 𝑏
resulting in the given complex number 𝐶. The unique complex number
𝑎 is 𝐶, and the unique another complex
number 𝑏 is 0.
Remark: This, together with addsqnreup 25721, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑). See also comments for df-eu 2584 and 2eu4 2686. For more details see comment for addsqnreup 25721. (Contributed by AV, 21-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqn2reu 25719* |
For each complex number 𝐶, there does not exist a unique
complex
number 𝑏, squared and added to a unique
another complex number
𝑎 resulting in the given complex number
𝐶.
Actually, for each
complex number 𝑏, 𝑎 = (𝐶 − (𝑏↑2)) is unique.
Remark: This, together with addsq2reu 25718, shows that commutation of two unique quantifications need not be equivalent, and provides an evident justification of the fact that considering the pair of variables is necessary to obtain what we intuitively understand as "double unique existence". (Proposed by GL, 23-Jun-2023.). (Contributed by AV, 23-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑏 ∈ ℂ ∃!𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqrexnreu 25720* |
For each complex number, there exists a complex number to which the
square of more than one (or no) other complex numbers can be added to
result in the given complex number.
Remark: This theorem, together with addsq2reu 25718, shows that there are cases in which there is a set together with a not unique other set fulfilling a wff, although there is a unique set fulfilling the wff together with another unique set (see addsq2reu 25718). For more details see comment for addsqnreup 25721. (Contributed by AV, 20-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqnreup 25721* |
There is no unique decomposition of a complex number as a sum of a
complex number and a square of a complex number.
Remark: This theorem, together with addsq2reu 25718, is a real life example (about a numerical property) showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑"). See also comments for df-eu 2584 and 2eu4 2686. In the case of decompositions of complex numbers as a sum of a complex number and a square of a complex number, the only/unique complex number to which the square of a unique complex number is added yields in the given complex number is the given number itself, and the unique complex number to be squared is 0 (see comment for addsq2reu 25718). There are, however, complex numbers to which the square of more than one other complex numbers can be added to yield the given complex number (see addsqrexnreu 25720). For example, 〈1, (√‘(𝐶 − 1))〉 and 〈1, -(√‘(𝐶 − 1))〉 are two different decompositions of 𝐶 (if 𝐶 ≠ 1). Therefore, there is no unique decomposition of any complex number as a sum of a complex number and a square of a complex number, as generally proved by this theorem. As a consequence, a theorem must claim the existence of a unique pair of sets to express "There are unique 𝑎 and 𝑏 so that .." (more formally ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 with 𝑝 = 〈𝑎, 𝑏〉), or by showing (∃!𝑥 ∈ 𝐴∃𝑦 ∈ 𝐵𝜑 ∧ ∃!𝑦 ∈ 𝐵∃𝑥 ∈ 𝐴𝜑) (see 2reu4 4349 resp. 2eu4 2686). These two representations are equivalent (see opreu2reurex 5983). An analogon of this theorem using the latter variant is given in addsqn2reurex2 25723. In some cases, however, the variant with (ordered!) pairs may be possible only for ordered sets (like ℝ or ℙ) and claiming that the first component is less than or equal to the second component (see, for example, 2sqreunnltb 25739 and 2sqreuopb 25746). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairsproper‘𝐴)𝜑 (see, for example, inlinecirc02preu 44149). (Contributed by AV, 21-Jun-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶) | ||
Theorem | addsq2nreurex 25722* | For each complex number 𝐶, there is no unique complex number 𝑎 added to the square of another complex number 𝑏 resulting in the given complex number 𝐶. (Contributed by AV, 2-Jul-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶) | ||
Theorem | addsqn2reurex2 25723* |
For each complex number 𝐶, there does not uniquely exist two
complex numbers 𝑎 and 𝑏, with 𝑏 squared
and added to 𝑎
resulting in the given complex number 𝐶.
Remark: This, together with addsq2reu 25718, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑), as it is the case with the pattern (∃!𝑎 ∈ 𝐴∃𝑏 ∈ 𝐵𝜑 ∧ ∃!𝑏 ∈ 𝐵∃𝑎 ∈ 𝐴𝜑. See also comments for df-eu 2584 and 2eu4 2686. (Contributed by AV, 2-Jul-2023.) |
⊢ (𝐶 ∈ ℂ → ¬ (∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ∧ ∃!𝑏 ∈ ℂ ∃𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)) | ||
Theorem | 2sqreulem1 25724* | Lemma 1 for 2sqreu 25734. (Contributed by AV, 4-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreultlem 25725* | Lemma for 2sqreult 25736. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreultblem 25726* | Lemma for 2sqreultb 25737. (Contributed by AV, 10-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
Theorem | 2sqreunnlem1 25727* | Lemma 1 for 2sqreunn 25735. (Contributed by AV, 11-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreunnltlem 25728* | Lemma for 2sqreunnlt 25738. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 11-Jun-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) | ||
Theorem | 2sqreunnltblem 25729* | Lemma for 2sqreunnltb 25739. (Contributed by AV, 11-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))) | ||
Theorem | 2sqreulem2 25730 | Lemma 2 for 2sqreu 25734 etc. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐶↑2)) → 𝐵 = 𝐶)) | ||
Theorem | 2sqreulem3 25731 | Lemma 3 for 2sqreu 25734 etc. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0)) → (((𝜑 ∧ ((𝐴↑2) + (𝐵↑2)) = 𝑃) ∧ (𝜓 ∧ ((𝐴↑2) + (𝐶↑2)) = 𝑃)) → 𝐵 = 𝐶)) | ||
Theorem | 2sqreulem4 25732* | Lemma 4 for 2sqreu 25734 et. (Contributed by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ0 ∃*𝑏 ∈ ℕ0 𝜑 | ||
Theorem | 2sqreunnlem2 25733* | Lemma 2 for 2sqreunn 25735. (Contributed by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ∀𝑎 ∈ ℕ ∃*𝑏 ∈ ℕ 𝜑 | ||
Theorem | 2sqreu 25734* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 25716 for the existence of such a decomposition. (Contributed by AV, 4-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑)) | ||
Theorem | 2sqreunn 25735* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. See 2sqnn 25717 for the existence of such a decomposition. (Contributed by AV, 11-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑)) | ||
Theorem | 2sqreult 25736* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑)) | ||
Theorem | 2sqreultb 25737* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). (Contributed by AV, 10-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 𝜑 ∧ ∃!𝑏 ∈ ℕ0 ∃𝑎 ∈ ℕ0 𝜑))) | ||
Theorem | 2sqreunnlt 25738* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. (Contributed by AV, 4-Jun-2023.) Specialization to different integers, proposed by GL. (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑)) | ||
Theorem | 2sqreunnltb 25739* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. (Contributed by AV, 11-Jun-2023.) The prime needs not be odd, as observed by WL. (Revised by AV, 25-Jun-2023.) |
⊢ (𝜑 ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)) ⇒ ⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ (∃!𝑎 ∈ ℕ ∃𝑏 ∈ ℕ 𝜑 ∧ ∃!𝑏 ∈ ℕ ∃𝑎 ∈ ℕ 𝜑))) | ||
Theorem | 2sqreuop 25740* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu 25734. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopnn 25741* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. Ordered pair variant of 2sqreunn 25735. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuoplt 25742* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 25736. (Contributed by AV, 2-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopltb 25743* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). Ordered pair variant of 2sqreultb 25737. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
Theorem | 2sqreuopnnlt 25744* | There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. Ordered pair variant of 2sqreunnlt 25738. (Contributed by AV, 3-Jul-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)) | ||
Theorem | 2sqreuopnnltb 25745* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Ordered pair variant of 2sqreunnltb 25739. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))) | ||
Theorem | 2sqreuopb 25746* | There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Alternate ordered pair variant of 2sqreunnltb 25739. (Contributed by AV, 3-Jul-2023.) |
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))) | ||
Theorem | chebbnd1lem1 25747 | Lemma for chebbnd1 25750: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 25571. (Note that the expression 𝐾 is actually equal to 2 · 𝑁, but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 25562, which shows that each term in the expansion ((2 · 𝑁)C𝑁) = ∏𝑝 ∈ ℙ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) is at most 2 · 𝑁, so that the sum really only has nonzero elements up to 2 · 𝑁, and since each term is at most 2 · 𝑁, after taking logs we get the inequality π(2 · 𝑁) · log(2 · 𝑁) ≤ log((2 · 𝑁)C𝑁), and bclbnd 25558 finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2016.) |
⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ⇒ ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁)))) | ||
Theorem | chebbnd1lem2 25748 | Lemma for chebbnd1 25750: Show that log(𝑁) / 𝑁 does not change too much between 𝑁 and 𝑀 = ⌊(𝑁 / 2). (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → ((log‘(2 · 𝑀)) / (2 · 𝑀)) < (2 · ((log‘𝑁) / 𝑁))) | ||
Theorem | chebbnd1lem3 25749 | Lemma for chebbnd1 25750: get a lower bound on π(𝑁) / (𝑁 / log(𝑁)) that is independent of 𝑁. (Contributed by Mario Carneiro, 21-Sep-2014.) |
⊢ 𝑀 = (⌊‘(𝑁 / 2)) ⇒ ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → (((log‘2) − (1 / (2 · e))) / 2) < ((π‘𝑁) · ((log‘𝑁) / 𝑁))) | ||
Theorem | chebbnd1 25750 | The Chebyshev bound: The function π(𝑥) is eventually lower bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function (𝑥 / log(𝑥)) / π(𝑥) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) | ||
Theorem | chtppilimlem1 25751 | Lemma for chtppilim 25753. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) & ⊢ (𝜑 → 𝑁 ∈ (2[,)+∞)) & ⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴)) ⇒ ⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁)) | ||
Theorem | chtppilimlem2 25752* | Lemma for chtppilim 25753. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) | ||
Theorem | chtppilim 25753 | The θ function is asymptotic to π(𝑥)log(𝑥), so it is sufficient to prove θ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1 | ||
Theorem | chto1ub 25754 | The θ function is upper bounded by a linear term. Corollary of chtub 25490. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
Theorem | chebbnd2 25755 | The Chebyshev bound, part 2: The function π(𝑥) is eventually upper bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function π(𝑥) / (𝑥 / log(𝑥)) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1) | ||
Theorem | chto1lb 25756 | The θ function is lower bounded by a linear term. Corollary of chebbnd1 25750. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) ∈ 𝑂(1) | ||
Theorem | chpchtlim 25757 | The ψ and θ functions are asymptotic to each other, so is sufficient to prove either θ(𝑥) / 𝑥 ⇝𝑟 1 or ψ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016.) |
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1 | ||
Theorem | chpo1ub 25758 | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) | ||
Theorem | chpo1ubb 25759* | The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥) | ||
Theorem | vmadivsum 25760* | The sum of the von Mangoldt function over 𝑛 is asymptotic to log𝑥 + 𝑂(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.) |
⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) | ||
Theorem | vmadivsumb 25761* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐 | ||
Theorem | rplogsumlem1 25762* | Lemma for rplogsum 25805. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2) | ||
Theorem | rplogsumlem2 25763* | Lemma for rplogsum 25805. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2) | ||
Theorem | dchrisum0lem1a 25764 | Lemma for dchrisum0lem1 25794. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋)))) | ||
Theorem | rpvmasumlem 25765* | Lemma for rpvmasum 25804. Calculate the "trivial case" estimate Σ𝑛 ≤ 𝑥( 1 (𝑛)Λ(𝑛) / 𝑛) = log𝑥 + 𝑂(1), where 1 (𝑥) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) | ||
Theorem | dchrisumlema 25766* | Lemma for dchrisum 25770. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ((𝐼 ∈ ℝ+ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴))) | ||
Theorem | dchrisumlem1 25767* | Lemma for dchrisum 25770. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | ||
Theorem | dchrisumlem2 25768* | Lemma for dchrisum 25770. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) & ⊢ (𝜑 → 𝑈 ∈ ℝ+) & ⊢ (𝜑 → 𝑀 ≤ 𝑈) & ⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1)) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝐼)) ⇒ ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴)) | ||
Theorem | dchrisumlem3 25769* | Lemma for dchrisum 25770. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
Theorem | dchrisum 25770* | If 𝑛 ∈ [𝑀, +∞) ↦ 𝐴(𝑛) is a positive decreasing function approaching zero, then the infinite sum Σ𝑛, 𝑋(𝑛)𝐴(𝑛) is convergent, with the partial sum Σ𝑛 ≤ 𝑥, 𝑋(𝑛)𝐴(𝑛) within 𝑂(𝐴(𝑀)) of the limit 𝑇. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴) & ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))) | ||
Theorem | dchrmusumlema 25771* | Lemma for dchrmusum 25802 and dchrisumn0 25799. Apply dchrisum 25770 for the function 1 / 𝑦. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) | ||
Theorem | dchrmusum2 25772* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded, provided that 𝑇 ≠ 0. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · 𝑇)) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumlem1 25773* | An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘𝑚) / 𝑚)))) | ||
Theorem | dchrvmasum2lem 25774* | Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 25773. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚)))) | ||
Theorem | dchrvmasum2if 25775* | Combine the results of dchrvmasumlem1 25773 and dchrvmasum2lem 25774 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝜓, (log‘𝐴), 0)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘if(𝜓, (𝐴 / 𝑑), 𝑚)) / 𝑚)))) | ||
Theorem | dchrvmasumlem2 25776* | Lemma for dchrvmasum 25803. (Contributed by Mario Carneiro, 4-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ) & ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumlem3 25777* | Lemma for dchrvmasum 25803. (Contributed by Mario Carneiro, 3-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ) & ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → 𝑇 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumlema 25778* | Lemma for dchrvmasum 25803 and dchrvmasumif 25781. Apply dchrisum 25770 for the function log(𝑦) / 𝑦, which is decreasing above e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 · ((log‘𝑦) / 𝑦)))) | ||
Theorem | dchrvmasumiflem1 25779* | Lemma for dchrvmasumif 25781. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumiflem2 25780* | Lemma for dchrvmasum 25803. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) | ||
Theorem | dchrvmasumif 25781* | An asymptotic approximation for the sum of 𝑋(𝑛)Λ(𝑛) / 𝑛 conditional on the value of the infinite sum 𝑆. (We will later show that the case 𝑆 = 0 is impossible, and hence establish dchrvmasum 25803.) (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) | ||
Theorem | dchrvmaeq0 25782* | The set 𝑊 is the collection of all non-principal Dirichlet characters such that the sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is equal to zero. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑊 ↔ 𝑆 = 0)) | ||
Theorem | dchrisum0fval 25783* | Value of the function 𝐹, the divisor sum of a Dirichlet character. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) ⇒ ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = Σ𝑡 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑡))) | ||
Theorem | dchrisum0fmul 25784* | The function 𝐹, the divisor sum of a Dirichlet character, is a multiplicative function (but not completely multiplicative). Equation 9.4.27 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) · (𝐹‘𝐵))) | ||
Theorem | dchrisum0ff 25785* | The function 𝐹 is a real function. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) ⇒ ⊢ (𝜑 → 𝐹:ℕ⟶ℝ) | ||
Theorem | dchrisum0flblem1 25786* | Lemma for dchrisum0flb 25788. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴))) | ||
Theorem | dchrisum0flblem2 25787* | Lemma for dchrisum0flb 25788. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝐴) & ⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦)) ⇒ ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴)) | ||
Theorem | dchrisum0flb 25788* | The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴)) | ||
Theorem | dchrisum0fno1 25789* | The sum Σ𝑘 ≤ 𝑥, 𝐹(𝑥) / √𝑘 is divergent (i.e. not eventually bounded). Equation 9.4.30 of [Shapiro], p. 383. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣))) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) & ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))((𝐹‘𝑘) / (√‘𝑘))) ∈ 𝑂(1)) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | rpvmasum2 25790* | A partial result along the lines of rpvmasum 25804. The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to (1 − 𝑀)(log𝑥 / ϕ(𝑥)) + 𝑂(1), where 𝑀 is the number of non-principal Dirichlet characters with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ 𝑈 = (Unit‘𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ 𝑇 = (◡𝐿 “ {𝐴}) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1)) | ||
Theorem | dchrisum0re 25791* | Suppose 𝑋 is a non-principal Dirichlet character with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Then 𝑋 is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ) | ||
Theorem | dchrisum0lema 25792* | Lemma for dchrisum0 25798. Apply dchrisum 25770 for the function 1 / √𝑦. (Contributed by Mario Carneiro, 10-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) ⇒ ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) | ||
Theorem | dchrisum0lem1b 25793* | Lemma for dchrisum0lem1 25794. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥))) | ||
Theorem | dchrisum0lem1 25794* | Lemma for dchrisum0 25798. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) | ||
Theorem | dchrisum0lem2a 25795* | Lemma for dchrisum0 25798. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) & ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) & ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1)) | ||
Theorem | dchrisum0lem2 25796* | Lemma for dchrisum0 25798. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) & ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) & ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) & ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) | ||
Theorem | dchrisum0lem3 25797* | Lemma for dchrisum0 25798. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)) | ||
Theorem | dchrisum0 25798* | The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 25772 and dchrvmasumif 25781. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} & ⊢ (𝜑 → 𝑋 ∈ 𝑊) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | dchrisumn0 25799* | The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 25772 and dchrvmasumif 25781. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → 𝑇 ≠ 0) | ||
Theorem | dchrmusumlem 25800* | The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.) |
⊢ 𝑍 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑍) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝐺 = (DChr‘𝑁) & ⊢ 𝐷 = (Base‘𝐺) & ⊢ 1 = (0g‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → 𝑋 ≠ 1 ) & ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) & ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) & ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦)) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((μ‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |