Home Metamath Proof ExplorerTheorem List (p. 206 of 309) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21328) Hilbert Space Explorer (21329-22851) Users' Mathboxes (22852-30843)

Theorem List for Metamath Proof Explorer - 20501-20600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdchrisum0 20501* 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 20475 and dchrvmasumif 20484. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
ℤ/n       RHom              DChr

Theoremdchrisumn0 20502* 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 20475 and dchrvmasumif 20484. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
ℤ/n       RHom              DChr

Theoremdchrmusumlem 20503* 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

Theoremdchrvmasumlem 20504* 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                                                               Λ

Theoremdchrmusum 20505* 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

Theoremdchrvmasum 20506* 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                                   Λ

Theoremrpvmasum 20507* The sum of the von Mangoldt function over those integers (mod ) is asymptotic to . 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                     Λ

Theoremrplogsum 20508* The sum of over the primes (mod ) is asymptotic to . Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.)
ℤ/n       RHom              Unit

Theoremdirith2 20509 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

Theoremdirith 20510* Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to . Theorem 9.4.1 of [Shapiro], p. 375. See http://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html for an informal exposition. (Contributed by Mario Carneiro, 12-May-2016.)

13.4.12  The Prime Number Theorem

Theoremmudivsum 20511* Asymptotic formula for . Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)

Theoremmulogsumlem 20512* Lemma for mulogsum 20513. (Contributed by Mario Carneiro, 14-May-2016.)

Theoremmulogsum 20513* Asymptotic formula for . Equation 10.2.6 of [Shapiro], p. 406. (Contributed by Mario Carneiro, 14-May-2016.)

Theoremlogdivsum 20514* Asymptotic analysis of . (Contributed by Mario Carneiro, 18-May-2016.)

Theoremmulog2sumlem1 20515* Asymptotic formula for , with explicit constants. Equation 10.2.7 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 18-May-2016.)

Theoremmulog2sumlem2 20516* Lemma for mulog2sum 20518. (Contributed by Mario Carneiro, 19-May-2016.)

Theoremmulog2sumlem3 20517* Lemma for mulog2sum 20518. (Contributed by Mario Carneiro, 13-May-2016.)

Theoremmulog2sum 20518* Asymptotic formula for . Equation 10.2.8 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 19-May-2016.)

Theoremvmalogdivsum2 20519* The sum Λ is asymptotic to . Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
Λ

Theoremvmalogdivsum 20520* The sum Λ is asymptotic to . Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
Λ

Λ        Λ Λ

Theorem2vmadivsum 20522* The sum ΛΛ is asymptotic to . (Contributed by Mario Carneiro, 30-May-2016.)
Λ Λ

Theoremlogsqvma 20523* A formula for in terms of the primes. Equation 10.4.6 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
Λ Λ Λ

Theoremlogsqvma2 20524* The Möbius inverse of logsqvma 20523. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
Λ Λ Λ

Theoremlog2sumbnd 20525* Bound on the difference between and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.)

Theoremselberglem1 20526* Lemma for selberg 20529. Estimation of the asymptotic part of selberglem3 20528. (Contributed by Mario Carneiro, 20-May-2016.)

Theoremselberglem2 20527* Lemma for selberg 20529. (Contributed by Mario Carneiro, 23-May-2016.)

Theoremselberglem3 20528* Lemma for selberg 20529. Estimation of the left hand side of logsqvma2 20524. (Contributed by Mario Carneiro, 23-May-2016.)

Theoremselberg 20529* Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that Λ ΛΛ . Equation 10.4.10 of [Shapiro], p. 419. (Contributed by Mario Carneiro, 23-May-2016.)
Λ ψ

Theoremselbergb 20530* Convert eventual boundedness in selberg 20529 to boundedness on . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016.)
Λ ψ

Theoremselberg2lem 20531* Lemma for selberg2 20532. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
Λ ψ

Theoremselberg2 20532* Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
ψ Λ ψ

Theoremselberg2b 20533* Convert eventual boundedness in selberg2 20532 to boundedness on any interval . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 25-May-2016.)
ψ Λ ψ

Theoremchpdifbndlem1 20534* Lemma for chpdifbnd 20536. (Contributed by Mario Carneiro, 25-May-2016.)
ψ Λ ψ                             ψ ψ

Theoremchpdifbndlem2 20535* Lemma for chpdifbnd 20536. (Contributed by Mario Carneiro, 25-May-2016.)
ψ Λ ψ               ψ ψ

Theoremchpdifbnd 20536* A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.)
ψ ψ

Theoremlogdivbnd 20537* A bound on a sum of logs, used in pntlemk 20587. This is not as precise as logdivsum 20514 in its asymptotic behavior, but it is valid for all and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016.)

Theoremselberg3lem1 20538* Introduce a log weighting on the summands of ΛΛ, the core of selberg2 20532 (written here as Λψ ). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Λ ψ        Λ ψ Λ ψ

Theoremselberg3lem2 20539* Lemma for selberg3 20540. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Λ ψ Λ ψ

Theoremselberg3 20540* Introduce a log weighting on the summands of ΛΛ, the core of selberg2 20532 (written here as Λψ ). Equation 10.6.7 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
ψ Λ ψ

Theoremselberg4lem1 20541* Lemma for selberg4 20542. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Λ ψ        Λ Λ ψ

Theoremselberg4 20542* The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form ΛΛΛ; we eliminate one of the nested sums by using the definition of ψ Λ. This statement can thus equivalently be written ψ ΛΛΛ . Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
ψ Λ Λ ψ

Theorempntrval 20543* Define the residual of the second Chebyshev function. The goal is to have , or . (Contributed by Mario Carneiro, 8-Apr-2016.)
ψ        ψ

Theorempntrf 20544 Functionality of the residual. Lemma for pnt 20595. (Contributed by Mario Carneiro, 8-Apr-2016.)
ψ

Theorempntrmax 20545* There is a bound on the residual valid for all . (Contributed by Mario Carneiro, 9-Apr-2016.)
ψ

Theorempntrsumo1 20546* A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
ψ

Theorempntrsumbnd 20547* A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
ψ

Theorempntrsumbnd2 20548* A bound on a sum over . Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ

Theoremselbergr 20549* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.)
ψ        Λ

Theoremselberg3r 20550* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.)
ψ        Λ

Theoremselberg4r 20551* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.)
ψ        Λ Λ

Theoremselberg34r 20552* The sum of selberg3r 20550 and selberg4r 20551. (Contributed by Mario Carneiro, 31-May-2016.)
ψ        Λ Λ Λ

Theorempntsval 20553* Define the "Selberg function", whose asymptotic behavior is the content of selberg 20529. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        Λ ψ

Theorempntsf 20554* Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ

Theoremselbergs 20555* Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ

Theoremselbergsb 20556* Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ

Theorempntsval2 20557* The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        Λ Λ Λ

Theorempntrlog2bndlem1 20558* The sum of selberg3r 20550 and selberg4r 20551. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ

Theorempntrlog2bndlem2 20559* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ               ψ

Theorempntrlog2bndlem3 20560* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ

Theorempntrlog2bndlem4 20561* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ

Theorempntrlog2bndlem5 20562* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ

Theorempntrlog2bndlem6a 20563* Lemma for pntrlog2bndlem6 20564. (Contributed by Mario Carneiro, 7-Jun-2016.)
Λ ψ        ψ

Theorempntrlog2bndlem6 20564* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Λ ψ        ψ

Theorempntrlog2bnd 20565* A bound on . Equation 10.6.15 of [Shapiro], p. 431. (Contributed by Mario Carneiro, 1-Jun-2016.)
ψ

Theorempntpbnd1a 20566* Lemma for pntpbnd 20569. (Contributed by Mario Carneiro, 11-Apr-2016.)
ψ

Theorempntpbnd1 20567* Lemma for pntpbnd 20569. (Contributed by Mario Carneiro, 11-Apr-2016.)
ψ

Theorempntpbnd2 20568* Lemma for pntpbnd 20569. (Contributed by Mario Carneiro, 11-Apr-2016.)
ψ

Theorempntpbnd 20569* Lemma for pnt 20595. Establish smallness of at a point. Lemma 10.6.1 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
ψ

Theorempntibndlem1 20570 Lemma for pntibnd 20574. (Contributed by Mario Carneiro, 10-Apr-2016.)
ψ

Theorempntibndlem2a 20571* Lemma for pntibndlem2 20572. (Contributed by Mario Carneiro, 7-Jun-2016.)
ψ

Theorempntibndlem2 20572* Lemma for pntibnd 20574. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
ψ                                                                              ψ ψ

Theorempntibndlem3 20573* Lemma for pntibnd 20574. Package up pntibndlem2 20572 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
ψ

Theorempntibnd 20574* Lemma for pnt 20595. Establish smallness of on an interval. Lemma 10.6.2 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
ψ

Theorempntlemd 20575 Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is C^*, is c1, is λ, is c2, and is c3. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;

Theorempntlemc 20576* Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is α, is ε, and is K. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;

Theorempntlema 20577* Lemma for pnt 20595. Closure for the constants used in the proof. The mammoth expression is a number large enough to satisfy all the lower bounds needed for . For comparison with Equation 10.6.27 of [Shapiro], p. 434, is x2, is x1, is the big-O constant in Equation 10.6.29 of [Shapiro], p. 435, and is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of [Shapiro], p. 436. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlemb 20578* Lemma for pnt 20595. Unpack all the lower bounds contained in , in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is x. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;               ;

Theorempntlemg 20579* Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is j^* and is ĵ. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlemh 20580* Lemma for pnt 20595. Bounds on the subintervals in the induction. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlemn 20581* Lemma for pnt 20595. The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlemq 20582* Lemma for pntlemj 20584. (Contributed by Mario Carneiro, 7-Jun-2016.)
ψ                                    ;                                                         ;                                                                ..^

Theorempntlemr 20583* Lemma for pntlemj 20584. (Contributed by Mario Carneiro, 7-Jun-2016.)
ψ                                    ;                                                         ;                                                                ..^

Theorempntlemj 20584* Lemma for pnt 20595. The induction step. Using pntibnd 20574, we find an interval in which is sufficiently large and has a much smaller value, (instead of our original bound ). (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;                                                                ..^

Theorempntlemi 20585* Lemma for pnt 20595. Eliminate some assumptions from pntlemj 20584. (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;                                                  ..^

Theorempntlemf 20586* Lemma for pnt 20595. Add up the pieces in pntlemi 20585 to get an estimate slightly better than the naive lower bound . (Contributed by Mario Carneiro, 13-Apr-2016.)
ψ                                    ;                                                         ;                                           ;

Theorempntlemk 20587* Lemma for pnt 20595. Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlemo 20588* Lemma for pnt 20595. Combine all the estimates to establish a smaller eventual bound on . (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntleme 20589* Lemma for pnt 20595. Package up pntlemo 20588 in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ                                    ;                                                         ;

Theorempntlem3 20590* Lemma for pnt 20595. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.)
ψ                                           ψ

Theorempntlemp 20591* Lemma for pnt 20595. Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ                                           ;

Theorempntleml 20592* Lemma for pnt 20595. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 14-Apr-2016.)
ψ