Home | Metamath
Proof Explorer Theorem List (p. 268 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2sqblem 26701 | Lemma for 2sqb 26702. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข (๐ โ (๐ โ โ โง ๐ โ 2)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข (๐ โ ๐ = ((๐โ2) + (๐โ2))) & โข (๐ โ ๐ด โ โค) & โข (๐ โ ๐ต โ โค) & โข (๐ โ (๐ gcd ๐) = ((๐ ยท ๐ด) + (๐ ยท ๐ต))) โ โข (๐ โ (๐ mod 4) = 1) | ||
Theorem | 2sqb 26702* | The converse to 2sq 26700. (Contributed by Mario Carneiro, 20-Jun-2015.) |
โข (๐ โ โ โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ = 2 โจ (๐ mod 4) = 1))) | ||
Theorem | 2sq2 26703 | 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 26704 | 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 26705 | 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 26706 | 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 26707* | There exists at most one decomposition of a prime as a sum of two squares. See 2sqb 26702 for the existence of such a decomposition. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
โข (๐ โ โ โ โ*๐ โ โ0 โ๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqnn0 26708* | 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 26709* | 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 26710* |
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 26713, is an example showing that the pattern โ!๐ โ ๐ดโ!๐ โ ๐ต๐ does not necessarily mean "There are unique sets ๐ and ๐ fulfilling ๐). See also comments for df-eu 2569 and 2eu4 2656. For more details see comment for addsqnreup 26713. (Contributed by AV, 21-Jun-2023.) |
โข (๐ถ โ โ โ โ!๐ โ โ โ!๐ โ โ (๐ + (๐โ2)) = ๐ถ) | ||
Theorem | addsqn2reu 26711* |
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 26710, 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 26712* |
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 26710, 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 26710). For more details see comment for addsqnreup 26713. (Contributed by AV, 20-Jun-2023.) |
โข (๐ถ โ โ โ โ๐ โ โ ยฌ โ!๐ โ โ (๐ + (๐โ2)) = ๐ถ) | ||
Theorem | addsqnreup 26713* |
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 26710, 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 2569 and 2eu4 2656. 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 26710). 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 26712). 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 4483 resp. 2eu4 2656). These two representations are equivalent (see opreu2reurex 6243). An analogon of this theorem using the latter variant is given in addsqn2reurex2 26715. 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 26731 and 2sqreuopb 26738). Alternatively, (proper) unordered pairs can be used: โ!๐๐๐ซ ๐ด((โฏโ๐) = 2 โง ๐), or, using the definition of proper pairs: โ!๐ โ (Pairsproperโ๐ด)๐ (see, for example, inlinecirc02preu 46574). (Contributed by AV, 21-Jun-2023.) |
โข (๐ถ โ โ โ ยฌ โ!๐ โ (โ ร โ)((1st โ๐) + ((2nd โ๐)โ2)) = ๐ถ) | ||
Theorem | addsq2nreurex 26714* | 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 26715* |
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 26710, 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 2569 and 2eu4 2656. (Contributed by AV, 2-Jul-2023.) |
โข (๐ถ โ โ โ ยฌ (โ!๐ โ โ โ๐ โ โ (๐ + (๐โ2)) = ๐ถ โง โ!๐ โ โ โ๐ โ โ (๐ + (๐โ2)) = ๐ถ)) | ||
Theorem | 2sqreulem1 26716* | Lemma 1 for 2sqreu 26726. (Contributed by AV, 4-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ0 โ!๐ โ โ0 (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreultlem 26717* | Lemma for 2sqreult 26728. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ0 โ!๐ โ โ0 (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreultblem 26718* | Lemma for 2sqreultb 26729. (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 26719* | Lemma 1 for 2sqreunn 26727. (Contributed by AV, 11-Jun-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ โ โ!๐ โ โ (๐ โค ๐ โง ((๐โ2) + (๐โ2)) = ๐)) | ||
Theorem | 2sqreunnltlem 26720* | Lemma for 2sqreunnlt 26730. (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 26721* | Lemma for 2sqreunnltb 26731. (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 26722 | Lemma 2 for 2sqreu 26726 etc. (Contributed by AV, 25-Jun-2023.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0 โง ๐ถ โ โ0) โ (((๐ดโ2) + (๐ตโ2)) = ((๐ดโ2) + (๐ถโ2)) โ ๐ต = ๐ถ)) | ||
Theorem | 2sqreulem3 26723 | Lemma 3 for 2sqreu 26726 etc. (Contributed by AV, 25-Jun-2023.) |
โข ((๐ด โ โ0 โง (๐ต โ โ0 โง ๐ถ โ โ0)) โ (((๐ โง ((๐ดโ2) + (๐ตโ2)) = ๐) โง (๐ โง ((๐ดโ2) + (๐ถโ2)) = ๐)) โ ๐ต = ๐ถ)) | ||
Theorem | 2sqreulem4 26724* | Lemma 4 for 2sqreu 26726 et. (Contributed by AV, 25-Jun-2023.) |
โข (๐ โ (๐ โง ((๐โ2) + (๐โ2)) = ๐)) โ โข โ๐ โ โ0 โ*๐ โ โ0 ๐ | ||
Theorem | 2sqreunnlem2 26725* | Lemma 2 for 2sqreunn 26727. (Contributed by AV, 25-Jun-2023.) |
โข (๐ โ (๐ โง ((๐โ2) + (๐โ2)) = ๐)) โ โข โ๐ โ โ โ*๐ โ โ ๐ | ||
Theorem | 2sqreu 26726* | There exists a unique decomposition of a prime of the form 4๐ + 1 as a sum of squares of two nonnegative integers. See 2sqnn0 26708 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 26727* | There exists a unique decomposition of a prime of the form 4๐ + 1 as a sum of squares of two positive integers. See 2sqnn 26709 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 26728* | 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 26729* | 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 26730* | 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 26731* | 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 26732* | 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 26726. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ0 ร โ0)((1st โ๐) โค (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopnn 26733* | 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 26727. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ ร โ)((1st โ๐) โค (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuoplt 26734* | There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 26728. (Contributed by AV, 2-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ0 ร โ0)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopltb 26735* | 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 26729. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ0 ร โ0)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐))) | ||
Theorem | 2sqreuopnnlt 26736* | 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 26730. (Contributed by AV, 3-Jul-2023.) |
โข ((๐ โ โ โง (๐ mod 4) = 1) โ โ!๐ โ (โ ร โ)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐)) | ||
Theorem | 2sqreuopnnltb 26737* | 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 26731. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ ร โ)((1st โ๐) < (2nd โ๐) โง (((1st โ๐)โ2) + ((2nd โ๐)โ2)) = ๐))) | ||
Theorem | 2sqreuopb 26738* | 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 26731. (Contributed by AV, 3-Jul-2023.) |
โข (๐ โ โ โ ((๐ mod 4) = 1 โ โ!๐ โ (โ ร โ)โ๐โ๐(๐ = โจ๐, ๐โฉ โง (๐ < ๐ โง ((๐โ2) + (๐โ2)) = ๐)))) | ||
Theorem | chebbnd1lem1 26739 | Lemma for chebbnd1 26742: show a lower bound on ฯ(๐ฅ) at even integers using similar techniques to those used to prove bpos 26563. (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 26554, 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 26550 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 26740 | Lemma for chebbnd1 26742: 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 26741 | Lemma for chebbnd1 26742: 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 26742 | 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 26743 | Lemma for chtppilim 26745. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ด < 1) & โข (๐ โ ๐ โ (2[,)+โ)) & โข (๐ โ ((๐โ๐๐ด) / (ฯโ๐)) < (1 โ ๐ด)) โ โข (๐ โ ((๐ดโ2) ยท ((ฯโ๐) ยท (logโ๐))) < (ฮธโ๐)) | ||
Theorem | chtppilimlem2 26744* | Lemma for chtppilim 26745. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ด < 1) โ โข (๐ โ โ๐ง โ โ โ๐ฅ โ (2[,)+โ)(๐ง โค ๐ฅ โ ((๐ดโ2) ยท ((ฯโ๐ฅ) ยท (logโ๐ฅ))) < (ฮธโ๐ฅ))) | ||
Theorem | chtppilim 26745 | 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 26746 | The ฮธ function is upper bounded by a linear term. Corollary of chtub 26482. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ฅ โ โ+ โฆ ((ฮธโ๐ฅ) / ๐ฅ)) โ ๐(1) | ||
Theorem | chebbnd2 26747 | 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 26748 | The ฮธ function is lower bounded by a linear term. Corollary of chebbnd1 26742. (Contributed by Mario Carneiro, 8-Apr-2016.) |
โข (๐ฅ โ (2[,)+โ) โฆ (๐ฅ / (ฮธโ๐ฅ))) โ ๐(1) | ||
Theorem | chpchtlim 26749 | 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 26750 | The ฯ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.) |
โข (๐ฅ โ โ+ โฆ ((ฯโ๐ฅ) / ๐ฅ)) โ ๐(1) | ||
Theorem | chpo1ubb 26751* | The ฯ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.) |
โข โ๐ โ โ+ โ๐ฅ โ โ+ (ฯโ๐ฅ) โค (๐ ยท ๐ฅ) | ||
Theorem | vmadivsum 26752* | 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 26753* | Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.) |
โข โ๐ โ โ+ โ๐ฅ โ (1[,)+โ)(absโ(ฮฃ๐ โ (1...(โโ๐ฅ))((ฮโ๐) / ๐) โ (logโ๐ฅ))) โค ๐ | ||
Theorem | rplogsumlem1 26754* | Lemma for rplogsum 26797. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ด โ โ โ ฮฃ๐ โ (2...๐ด)((logโ๐) / (๐ ยท (๐ โ 1))) โค 2) | ||
Theorem | rplogsumlem2 26755* | Lemma for rplogsum 26797. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ด โ โค โ ฮฃ๐ โ (1...๐ด)(((ฮโ๐) โ if(๐ โ โ, (logโ๐), 0)) / ๐) โค 2) | ||
Theorem | dchrisum0lem1a 26756 | Lemma for dchrisum0lem1 26786. (Contributed by Mario Carneiro, 7-Jun-2016.) |
โข (((๐ โง ๐ โ โ+) โง ๐ท โ (1...(โโ๐))) โ (๐ โค ((๐โ2) / ๐ท) โง (โโ((๐โ2) / ๐ท)) โ (โคโฅโ(โโ๐)))) | ||
Theorem | rpvmasumlem 26757* | Lemma for rpvmasum 26796. 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 26758* | Lemma for dchrisum 26762. 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 26759* | Lemma for dchrisum 26762. 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 26760* | Lemma for dchrisum 26762. 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 26761* | Lemma for dchrisum 26762. 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 26762* | 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 26763* | Lemma for dchrmusum 26794 and dchrisumn0 26791. Apply dchrisum 26762 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 26764* | 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 26765* | 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 26766* | Give an expression for log๐ฅ remarkably similar to ฮฃ๐ โค ๐ฅ(๐(๐)ฮ(๐) / ๐) given in dchrvmasumlem1 26765. 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 26767* | Combine the results of dchrvmasumlem1 26765 and dchrvmasum2lem 26766 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 26768* | Lemma for dchrvmasum 26795. (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 26769* | Lemma for dchrvmasum 26795. (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 26770* | Lemma for dchrvmasum 26795 and dchrvmasumif 26773. Apply dchrisum 26762 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 26771* | Lemma for dchrvmasumif 26773. (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 26772* | Lemma for dchrvmasum 26795. (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 26773* | 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 26795.) (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 26774* | 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 26775* | 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 26776* | 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 26777* | The function ๐น is a real function. (Contributed by Mario Carneiro, 5-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐บ = (DChrโ๐) & โข ๐ท = (Baseโ๐บ) & โข 1 = (0gโ๐บ) & โข ๐น = (๐ โ โ โฆ ฮฃ๐ฃ โ {๐ โ โ โฃ ๐ โฅ ๐} (๐โ(๐ฟโ๐ฃ))) & โข (๐ โ ๐ โ ๐ท) & โข (๐ โ ๐:(Baseโ๐)โถโ) โ โข (๐ โ ๐น:โโถโ) | ||
Theorem | dchrisum0flblem1 26778* | Lemma for dchrisum0flb 26780. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐บ = (DChrโ๐) & โข ๐ท = (Baseโ๐บ) & โข 1 = (0gโ๐บ) & โข ๐น = (๐ โ โ โฆ ฮฃ๐ฃ โ {๐ โ โ โฃ ๐ โฅ ๐} (๐โ(๐ฟโ๐ฃ))) & โข (๐ โ ๐ โ ๐ท) & โข (๐ โ ๐:(Baseโ๐)โถโ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ โ0) โ โข (๐ โ if((โโ(๐โ๐ด)) โ โ, 1, 0) โค (๐นโ(๐โ๐ด))) | ||
Theorem | dchrisum0flblem2 26779* | Lemma for dchrisum0flb 26780. 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 26780* | 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 26781* | 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 26782* | A partial result along the lines of rpvmasum 26796. 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 26783* | 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 26784* | Lemma for dchrisum0 26790. Apply dchrisum 26762 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 26785* | Lemma for dchrisum0lem1 26786. (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 26786* | Lemma for dchrisum0 26790. (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 26787* | Lemma for dchrisum0 26790. (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 26788* | Lemma for dchrisum0 26790. (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 26789* | Lemma for dchrisum0 26790. (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 26790* | 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 26764 and dchrvmasumif 26773. 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 26791* | 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 26764 and dchrvmasumif 26773. 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 26792* | 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)) | ||
Theorem | dchrvmasumlem 26793* | 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)) | ||
Theorem | dchrmusum 26794* | 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 ) โ โข (๐ โ (๐ฅ โ โ+ โฆ ฮฃ๐ โ (1...(โโ๐ฅ))((๐โ(๐ฟโ๐)) ยท ((ฮผโ๐) / ๐))) โ ๐(1)) | ||
Theorem | dchrvmasum 26795* | The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by ๐, is bounded. Equation 9.4.8 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 12-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐บ = (DChrโ๐) & โข ๐ท = (Baseโ๐บ) & โข 1 = (0gโ๐บ) & โข (๐ โ ๐ โ ๐ท) & โข (๐ โ ๐ โ 1 ) โ โข (๐ โ (๐ฅ โ โ+ โฆ ฮฃ๐ โ (1...(โโ๐ฅ))((๐โ(๐ฟโ๐)) ยท ((ฮโ๐) / ๐))) โ ๐(1)) | ||
Theorem | rpvmasum 26796* | The sum of the von Mangoldt function over those integers ๐โก๐ด (mod ๐) is asymptotic to log๐ฅ / ฯ(๐ฅ) + ๐(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐ = (Unitโ๐) & โข (๐ โ ๐ด โ ๐) & โข ๐ = (โก๐ฟ โ {๐ด}) โ โข (๐ โ (๐ฅ โ โ+ โฆ (((ฯโ๐) ยท ฮฃ๐ โ ((1...(โโ๐ฅ)) โฉ ๐)((ฮโ๐) / ๐)) โ (logโ๐ฅ))) โ ๐(1)) | ||
Theorem | rplogsum 26797* | The sum of log๐ / ๐ over the primes ๐โก๐ด (mod ๐) is asymptotic to log๐ฅ / ฯ(๐ฅ) + ๐(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐ = (Unitโ๐) & โข (๐ โ ๐ด โ ๐) & โข ๐ = (โก๐ฟ โ {๐ด}) โ โข (๐ โ (๐ฅ โ โ+ โฆ (((ฯโ๐) ยท ฮฃ๐ โ ((1...(โโ๐ฅ)) โฉ (โ โฉ ๐))((logโ๐) / ๐)) โ (logโ๐ฅ))) โ ๐(1)) | ||
Theorem | dirith2 26798 | Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to ๐. Theorem 9.4.1 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
โข ๐ = (โค/nโคโ๐) & โข ๐ฟ = (โคRHomโ๐) & โข (๐ โ ๐ โ โ) & โข ๐ = (Unitโ๐) & โข (๐ โ ๐ด โ ๐) & โข ๐ = (โก๐ฟ โ {๐ด}) โ โข (๐ โ (โ โฉ ๐) โ โ) | ||
Theorem | dirith 26799* | Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to ๐. Theorem 9.4.1 of [Shapiro], p. 375. See https://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html for an informal exposition. This is Metamath 100 proof #48. (Contributed by Mario Carneiro, 12-May-2016.) |
โข ((๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1) โ {๐ โ โ โฃ ๐ โฅ (๐ โ ๐ด)} โ โ) | ||
Theorem | mudivsum 26800* | Asymptotic formula for ฮฃ๐ โค ๐ฅ, ฮผ(๐) / ๐ = ๐(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.) |
โข (๐ฅ โ โ+ โฆ ฮฃ๐ โ (1...(โโ๐ฅ))((ฮผโ๐) / ๐)) โ ๐(1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |