P. 277 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27601-27700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2sqlem5 27601	Lemma for 2sq 27609. If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (𝑁 · 𝑃) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑁 ∈ 𝑆)
Theorem	2sqlem6 27602*	Lemma for 2sq 27609. 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 27603*	Lemma for 2sq 27609. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ 𝑌 ⊆ (𝑆 ∩ ℕ)
Theorem	2sqlem8a 27604*	Lemma for 2sqlem8 27605. (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 27605*	Lemma for 2sq 27609. (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 27606*	Lemma for 2sq 27609. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    &   ⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆))    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑌)    ⇒   ⊢ (𝜑 → 𝑀 ∈ 𝑆)
Theorem	2sqlem10 27607*	Lemma for 2sq 27609. 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 27608*	Lemma for 2sq 27609. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2))    &   ⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))}    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → 𝑃 ∈ 𝑆)
Theorem	2sq 27609*	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 27610	Lemma for 2sqb 27611. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))    &   ⊢ (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))    &   ⊢ (𝜑 → 𝑃 = ((𝑋↑2) + (𝑌↑2)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵)))    ⇒   ⊢ (𝜑 → (𝑃 mod 4) = 1)
Theorem	2sqb 27611*	The converse to 2sq 27609. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑃 ∈ ℙ → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑃 = ((𝑥↑2) + (𝑦↑2)) ↔ (𝑃 = 2 ∨ (𝑃 mod 4) = 1)))
Theorem	2sq2 27612	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 27613	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 27614	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 27615	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 27616*	There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 27611 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ (𝑃 ∈ ℙ → ∃*𝑎 ∈ ℕ0 ∃𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqnn0 27617*	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 27618*	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 27619*	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 27622, is an example showing that the pattern ∃!𝑎 ∈ 𝐴∃!𝑏 ∈ 𝐵𝜑 does not necessarily mean "There are unique sets 𝑎 and 𝑏 fulfilling 𝜑). See also comments for df-eu 2600 and 2eu4 2685. For more details see comment for addsqnreup 27622. (Contributed by AV, 21-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ∃!𝑎 ∈ ℂ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)
Theorem	addsqn2reu 27620*	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 27619, 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 27621*	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 27619, 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 27619). For more details see comment for addsqnreup 27622. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ∃𝑎 ∈ ℂ ¬ ∃!𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶)
Theorem	addsqnreup 27622*	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 27619, 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 2600 and 2eu4 2685. 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 27619). 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 27621). 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 4488 resp. 2eu4 2685). These two representations are equivalent (see opreu2reurex 6299). An analogon of this theorem using the latter variant is given in addsqn2reurex2 27624. 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 27640 and 2sqreuopb 27647). Alternatively, (proper) unordered pairs can be used: ∃!𝑝𝑒𝒫 𝐴((♯‘𝑝) = 2 ∧ 𝜑), or, using the definition of proper pairs: ∃!𝑝 ∈ (Pairsproper‘𝐴)𝜑 (see, for example, inlinecirc02preu 49600). (Contributed by AV, 21-Jun-2023.)
⊢ (𝐶 ∈ ℂ → ¬ ∃!𝑝 ∈ (ℂ × ℂ)((1st ‘𝑝) + ((2nd ‘𝑝)↑2)) = 𝐶)
Theorem	addsq2nreurex 27623*	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 27624*	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 27619, 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 2600 and 2eu4 2685. (Contributed by AV, 2-Jul-2023.)
⊢ (𝐶 ∈ ℂ → ¬ (∃!𝑎 ∈ ℂ ∃𝑏 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶 ∧ ∃!𝑏 ∈ ℂ ∃𝑎 ∈ ℂ (𝑎 + (𝑏↑2)) = 𝐶))
Theorem	2sqreulem1 27625*	Lemma 1 for 2sqreu 27635. (Contributed by AV, 4-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreultlem 27626*	Lemma for 2sqreult 27637. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreultblem 27627*	Lemma for 2sqreultb 27638. (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 27628*	Lemma 1 for 2sqreunn 27636. (Contributed by AV, 11-Jun-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ ∃!𝑏 ∈ ℕ (𝑎 ≤ 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Theorem	2sqreunnltlem 27629*	Lemma for 2sqreunnlt 27639. (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 27630*	Lemma for 2sqreunnltb 27640. (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 27631	Lemma 2 for 2sqreu 27635 etc. (Contributed by AV, 25-Jun-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → (((𝐴↑2) + (𝐵↑2)) = ((𝐴↑2) + (𝐶↑2)) → 𝐵 = 𝐶))
Theorem	2sqreulem3 27632	Lemma 3 for 2sqreu 27635 etc. (Contributed by AV, 25-Jun-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ (𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0)) → (((𝜑 ∧ ((𝐴↑2) + (𝐵↑2)) = 𝑃) ∧ (𝜓 ∧ ((𝐴↑2) + (𝐶↑2)) = 𝑃)) → 𝐵 = 𝐶))
Theorem	2sqreulem4 27633*	Lemma 4 for 2sqreu 27635 et. (Contributed by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ∀𝑎 ∈ ℕ0 ∃*𝑏 ∈ ℕ0 𝜑
Theorem	2sqreunnlem2 27634*	Lemma 2 for 2sqreunn 27636. (Contributed by AV, 25-Jun-2023.)
⊢ (𝜑 ↔ (𝜓 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))    ⇒   ⊢ ∀𝑎 ∈ ℕ ∃*𝑏 ∈ ℕ 𝜑
Theorem	2sqreu 27635*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 27617 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 27636*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. See 2sqnn 27618 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 27637*	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 27638*	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 27639*	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 27640*	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 27641*	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 27635. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopnn 27642*	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 27636. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuoplt 27643*	There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 27637. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopltb 27644*	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 27638. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)))
Theorem	2sqreuopnnlt 27645*	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 27639. (Contributed by AV, 3-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopnnltb 27646*	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 27640. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)))
Theorem	2sqreuopb 27647*	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 27640. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))))
14.4.12  Chebyshev's Weak Prime Number Theorem, Dirichlet's Theorem
Theorem	chebbnd1lem1 27648	Lemma for chebbnd1 27651: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 27472. (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 27463, 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 27459 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 27649	Lemma for chebbnd1 27651: 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 27650	Lemma for chebbnd1 27651: 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 27651	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 27652	Lemma for chtppilim 27654. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝑁 ∈ (2[,)+∞))    &   ⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴))    ⇒   ⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁))
Theorem	chtppilimlem2 27653*	Lemma for chtppilim 27654. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
Theorem	chtppilim 27654	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 27655	The θ function is upper bounded by a linear term. Corollary of chtub 27391. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)
Theorem	chebbnd2 27656	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 27657	The θ function is lower bounded by a linear term. Corollary of chebbnd1 27651. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) ∈ 𝑂(1)
Theorem	chpchtlim 27658	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 27659	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
Theorem	chpo1ubb 27660*	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥)
Theorem	vmadivsum 27661*	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 27662*	Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐
Theorem	rplogsumlem1 27663*	Lemma for rplogsum 27706. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2)
Theorem	rplogsumlem2 27664*	Lemma for rplogsum 27706. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Theorem	dchrisum0lem1a 27665	Lemma for dchrisum0lem1 27695. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋))))
Theorem	rpvmasumlem 27666*	Lemma for rpvmasum 27705. 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 27667*	Lemma for dchrisum 27671. 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 27668*	Lemma for dchrisum 27671. 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 27669*	Lemma for dchrisum 27671. 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 27670*	Lemma for dchrisum 27671. 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 27671*	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 27672*	Lemma for dchrmusum 27703 and dchrisumn0 27700. Apply dchrisum 27671 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 27673*	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 27674*	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 27675*	Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 27674. 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 27676*	Combine the results of dchrvmasumlem1 27674 and dchrvmasum2lem 27675 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 27677*	Lemma for dchrvmasum 27704. (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 27678*	Lemma for dchrvmasum 27704. (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 27679*	Lemma for dchrvmasum 27704 and dchrvmasumif 27682. Apply dchrisum 27671 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 27680*	Lemma for dchrvmasumif 27682. (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 27681*	Lemma for dchrvmasum 27704. (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 27682*	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 27704.) (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 27683*	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 27684*	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 27685*	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 27686*	The function 𝐹 is a real function. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶ℝ)
Theorem	dchrisum0flblem1 27687*	Lemma for dchrisum0flb 27689. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴)))
Theorem	dchrisum0flblem2 27688*	Lemma for dchrisum0flb 27689. 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 27689*	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 27690*	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 27691*	A partial result along the lines of rpvmasum 27705. 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 27692*	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 27693*	Lemma for dchrisum0 27699. Apply dchrisum 27671 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 27694*	Lemma for dchrisum0lem1 27695. (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 27695*	Lemma for dchrisum0 27699. (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 27696*	Lemma for dchrisum0 27699. (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 27697*	Lemma for dchrisum0 27699. (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 27698*	Lemma for dchrisum0 27699. (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 27699*	The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27673 and dchrvmasumif 27682. 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 27700*	The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27673 and dchrvmasumif 27682. 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)