P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dchrmusumlema 23401*	Lemma for dchrmusum 23432 and dchrisumn0 23429. Apply dchrisum 23400 for the function 1 / y. (Contributed by Mario Carneiro, 4-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   =>    |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) )
Theorem	dchrmusum2 23402*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n, is bounded, provided that T =/= 0. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> T )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. O(1) )
Theorem	dchrvmasumlem1 23403*	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.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- ( ph -> A e. RR+ )   =>    |- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` m ) / m ) ) ) )
Theorem	dchrvmasum2lem 23404*	Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n )Λ ( n ) / n ) given in dchrvmasumlem1 23403. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> ( log ` A ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` ( ( A / d ) / m ) ) / m ) ) ) )
Theorem	dchrvmasum2if 23405*	Combine the results of dchrvmasumlem1 23403 and dchrvmasum2lem 23404 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( ps , ( log ` A ) , 0 ) ) = sum_ d e. ( 1 ... ( |_ ` A ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) ( ( X ` ( L ` m ) ) x. ( ( log ` if ( ps , ( A / d ) , m ) ) / m ) ) ) )
Theorem	dchrvmasumlem2 23406*	Lemma for dchrvmasum 23433. (Contributed by Mario Carneiro, 4-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- ( ( ph /\ m e. RR+ ) -> F e. CC )   &    |- ( m = ( x / d ) -> F = K )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> T e. CC )   &    |- ( ( ph /\ m e. ( 3 [,) +oo ) ) -> ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )   &    |- ( ph -> R e. RR )   &    |- ( ph -> A. m e. ( 1 [,) 3 ) ( abs ` ( F - T ) ) <_ R )   =>    |- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) e. O(1) )
Theorem	dchrvmasumlem3 23407*	Lemma for dchrvmasum 23433. (Contributed by Mario Carneiro, 3-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- ( ( ph /\ m e. RR+ ) -> F e. CC )   &    |- ( m = ( x / d ) -> F = K )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> T e. CC )   &    |- ( ( ph /\ m e. ( 3 [,) +oo ) ) -> ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )   &    |- ( ph -> R e. RR )   &    |- ( ph -> A. m e. ( 1 [,) 3 ) ( abs ` ( F - T ) ) <_ R )   =>    |- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) e. O(1) )
Theorem	dchrvmasumlema 23408*	Lemma for dchrvmasum 23433 and dchrvmasumif 23411. Apply dchrisum 23400 for the function log ( y ) / y, which is decreasing above _e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )   =>    |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c x. ( ( log ` y ) / y ) ) ) )
Theorem	dchrvmasumiflem1 23409*	Lemma for dchrvmasumif 23411. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )   &    |- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )   &    |- ( ph -> E e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , K ) ~~> T )   &    |- ( ph -> A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E x. ( ( log ` y ) / y ) ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( sum_ k e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` k ) ) x. ( ( log ` if ( S = 0 , ( x / d ) , k ) ) / k ) ) - if ( S = 0 , 0 , T ) ) ) ) e. O(1) )
Theorem	dchrvmasumiflem2 23410*	Lemma for dchrvmasum 23433. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )   &    |- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( ( log ` a ) / a ) ) )   &    |- ( ph -> E e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , K ) ~~> T )   &    |- ( ph -> A. y e. ( 3 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E x. ( ( log ` y ) / y ) ) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
Theorem	dchrvmasumif 23411*	An asymptotic approximation for the sum of X ( n )Λ ( n ) / n conditional on the value of the infinite sum S. (We will later show that the case S = 0 is impossible, and hence establish dchrvmasum 23433.) (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) + if ( S = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
Theorem	dchrvmaeq0 23412*	The set W is the collection of all non-principal Dirichlet characters such that the sum sum_ n e. NN , X ( n ) / n is equal to zero. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / y ) )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   =>    |- ( ph -> ( X e. W <-> S = 0 ) )
Theorem	dchrisum0fval 23413*	Value of the function F, the divisor sum of a Dirichlet character. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   =>    |- ( A e. NN -> ( F ` A ) = sum_ t e. { q e. NN | q || A } ( X ` ( L ` t ) ) )
Theorem	dchrisum0fmul 23414*	The function F, 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.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( A gcd B ) = 1 )   =>    |- ( ph -> ( F ` ( A x. B ) ) = ( ( F ` A ) x. ( F ` B ) ) )
Theorem	dchrisum0ff 23415*	The function F is a real function. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> X : ( Base ` Z ) --> RR )   =>    |- ( ph -> F : NN --> RR )
Theorem	dchrisum0flblem1 23416*	Lemma for dchrisum0flb 23418. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> X : ( Base ` Z ) --> RR )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> A e. NN0 )   =>    |- ( ph -> if ( ( sqr ` ( P ^ A ) ) e. NN , 1 , 0 ) <_ ( F ` ( P ^ A ) ) )
Theorem	dchrisum0flblem2 23417*	Lemma for dchrisum0flb 23418. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> X : ( Base ` Z ) --> RR )   &    |- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> P || A )   &    |- ( ph -> A. y e. ( 1..^ A ) if ( ( sqr ` y ) e. NN , 1 , 0 ) <_ ( F ` y ) )   =>    |- ( ph -> if ( ( sqr ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) )
Theorem	dchrisum0flb 23418*	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.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> X : ( Base ` Z ) --> RR )   &    |- ( ph -> A e. NN )   =>    |- ( ph -> if ( ( sqr ` A ) e. NN , 1 , 0 ) <_ ( F ` A ) )
Theorem	dchrisum0fno1 23419*	The sum sum_ k <_ x , F ( x ) / sqr k is divergent (i.e. not eventually bounded). Equation 9.4.30 of [Shapiro], p. 383. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )   &    |- ( ph -> X e. D )   &    |- ( ph -> X : ( Base ` Z ) --> RR )   &    |- ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqr ` k ) ) ) e. O(1) )   =>    |- -. ph
Theorem	rpvmasum2 23420*	A partial result along the lines of rpvmasum 23434. The sum of the von Mangoldt function over those integers n == A (mod N) is asymptotic to ( 1 - M ) ( log x / phi ( x ) ) + O(1), where M is the number of non-principal Dirichlet characters with sum_ n e. NN , X ( n ) / n = 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.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   &    |- T = ( `' L " { A } )   &    |- ( ( ph /\ f e. W ) -> A = ( 1r ` Z ) )   =>    |- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) e. O(1) )
Theorem	dchrisum0re 23421*	Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0. Then X is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   =>    |- ( ph -> X : ( Base ` Z ) --> RR )
Theorem	dchrisum0lema 23422*	Lemma for dchrisum0 23428. Apply dchrisum 23400 for the function 1 / sqr y. (Contributed by Mario Carneiro, 10-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   =>    |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / ( sqr ` y ) ) ) )
Theorem	dchrisum0lem1b 23423*	Lemma for dchrisum0lem1 23424. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )   =>    |- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) ) <_ ( ( 2 x. C ) / ( sqr ` x ) ) )
Theorem	dchrisum0lem1 23424*	Lemma for dchrisum0 23428. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) ) e. O(1) )
Theorem	dchrisum0lem2a 23425*	Lemma for dchrisum0 23428. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )   &    |- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) )   &    |- ( ph -> H ~~> r U )   =>    |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) e. O(1) )
Theorem	dchrisum0lem2 23426*	Lemma for dchrisum0 23428. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )   &    |- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqr ` d ) ) - ( 2 x. ( sqr ` y ) ) ) )   &    |- ( ph -> H ~~> r U )   &    |- K = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> E e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , K ) ~~> T )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , K ) ` ( |_ ` y ) ) - T ) ) <_ ( E / y ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqr ` m ) ) / ( sqr ` d ) ) ) e. O(1) )
Theorem	dchrisum0lem3 23427*	Lemma for dchrisum0 23428. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqr ` a ) ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> S )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqr ` y ) ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqr ` ( m x. d ) ) ) ) e. O(1) )
Theorem	dchrisum0 23428*	The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 23402 and dchrvmasumif 23411. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }   &    |- ( ph -> X e. W )   =>    |- -. ph
Theorem	dchrisumn0 23429*	The sum sum_ n e. NN , X ( n ) / n is nonzero for all non-principal Dirichlet characters (i.e. the assumption X e. W is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 23402 and dchrvmasumif 23411. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> T )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )   =>    |- ( ph -> T =/= 0 )
Theorem	dchrmusumlem 23430*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> T )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) ) e. O(1) )
Theorem	dchrvmasumlem 23431*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   &    |- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )   &    |- ( ph -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> seq 1 ( + , F ) ~~> T )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )   =>    |- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. O(1) )
Theorem	dchrmusum 23432*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   =>    |- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) ) e. O(1) )
Theorem	dchrvmasum 23433*	The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by n, is bounded. Equation 9.4.8 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 12-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> X =/= .1. )   =>    |- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) ) e. O(1) )
Theorem	rpvmasum 23434*	The sum of the von Mangoldt function over those integers n == A (mod N) is asymptotic to log x / phi ( x ) + O(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   &    |- T = ( `' L " { A } )   =>    |- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
Theorem	rplogsum 23435*	The sum of log p / p over the primes p == A (mod N) is asymptotic to log x / phi ( x ) + O(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   &    |- T = ( `' L " { A } )   =>    |- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) e. O(1) )
Theorem	dirith2 23436	Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to N. Theorem 9.4.1 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   &    |- T = ( `' L " { A } )   =>    |- ( ph -> ( Prime i^i T ) ~~ NN )
Theorem	dirith 23437*	Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to N. Theorem 9.4.1 of [Shapiro], p. 375. See http://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.)
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> { p e. Prime | N || ( p - A ) } ~~ NN )
14.4.12  The Prime Number Theorem
Theorem	mudivsum 23438*	Asymptotic formula for sum_ n <_ x , mmu ( n ) / n = O(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1)
Theorem	mulogsumlem 23439*	Lemma for mulogsum 23440. (Contributed by Mario Carneiro, 14-May-2016.)
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) e. O(1)
Theorem	mulogsum 23440*	Asymptotic formula for sum_ n <_ x , ( mmu ( n ) / n ) log ( x / n ) = O(1). Equation 10.2.6 of [Shapiro], p. 406. (Contributed by Mario Carneiro, 14-May-2016.)
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1)
Theorem	logdivsum 23441*	Asymptotic analysis of sum_ n <_ x , log n / n = ( log x ) ^ 2 / 2 + L + O ( log x / x ). (Contributed by Mario Carneiro, 18-May-2016.)
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )   =>    |- ( F : RR+ --> RR /\ F e. dom ~~> r /\ ( ( F ~~> r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) )
Theorem	mulog2sumlem1 23442*	Asymptotic formula for sum_ n <_ x , log ( x / n ) / n = ( 1 / 2 ) log ^ 2 ( x ) + gamma x. log x - L + O ( log x / x ), with explicit constants. Equation 10.2.7 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 18-May-2016.)
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )   &    |- ( ph -> F ~~> r L )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> _e <_ A )   =>    |- ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) <_ ( 2 x. ( ( log ` A ) / A ) ) )
Theorem	mulog2sumlem2 23443*	Lemma for mulog2sum 23445. (Contributed by Mario Carneiro, 19-May-2016.)
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )   &    |- ( ph -> F ~~> r L )   &    |- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) )   &    |- R = ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) e. O(1) )
Theorem	mulog2sumlem3 23444*	Lemma for mulog2sum 23445. (Contributed by Mario Carneiro, 13-May-2016.)
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )   &    |- ( ph -> F ~~> r L )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
Theorem	mulog2sum 23445*	Asymptotic formula for sum_ n <_ x , ( mmu ( n ) / n ) log ^ 2 ( x / n ) = 2 log x + O(1). Equation 10.2.8 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 19-May-2016.)
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	vmalogdivsum2 23446*	The sum sum_ n <_ x , Λ ( n ) log ( x / n ) / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
Theorem	vmalogdivsum 23447*	The sum sum_ n <_ x , Λ ( n ) log n / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
Theorem	2vmadivsumlem 23448*	Lemma for 2vmadivsum 23449. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) / i ) - ( log ` y ) ) ) <_ A )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
Theorem	2vmadivsum 23449*	The sum sum_ m n <_ x , Λ ( m )Λ ( n ) / m n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ). (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
Theorem	logsqvma 23450*	A formula for log ^ 2 ( N ) in terms of the primes. Equation 10.4.6 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( sum_ u e. { x e. NN | x || d } ( (Λ ` u ) x. (Λ ` ( d / u ) ) ) + ( (Λ ` d ) x. ( log ` d ) ) ) = ( ( log ` N ) ^ 2 ) )
Theorem	logsqvma2 23451*	The Möbius inverse of logsqvma 23450. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) = ( sum_ d e. { x e. NN | x || N } ( (Λ ` d ) x. (Λ ` ( N / d ) ) ) + ( (Λ ` N ) x. ( log ` N ) ) ) )
Theorem	log2sumbnd 23452*	Bound on the difference between sum_ n <_ A , log ^ 2 ( n ) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.)
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( log ` n ) ^ 2 ) - ( A x. ( ( ( log ` A ) ^ 2 ) + ( 2 - ( 2 x. ( log ` A ) ) ) ) ) ) ) <_ ( ( ( log ` A ) ^ 2 ) + 2 ) )
Theorem	selberglem1 23453*	Lemma for selberg 23456. Estimation of the asymptotic part of selberglem3 23455. (Contributed by Mario Carneiro, 20-May-2016.)
|- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n )   =>    |- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selberglem2 23454*	Lemma for selberg 23456. (Contributed by Mario Carneiro, 23-May-2016.)
|- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n )   =>    |- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selberglem3 23455*	Lemma for selberg 23456. Estimation of the left-hand side of logsqvma2 23451. (Contributed by Mario Carneiro, 23-May-2016.)
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selberg 23456*	Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that sum_ n <_ x , Λ ( n ) log n + sum_ m x. n <_ x , Λ ( m )Λ ( n ) = 2 x log x + O ( x ). Equation 10.4.10 of [Shapiro], p. 419. (Contributed by Mario Carneiro, 23-May-2016.)
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( log ` n ) + (ψ ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selbergb 23457*	Convert eventual boundedness in selberg 23456 to boundedness on [ 1 , +oo ). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016.)
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( log ` n ) + (ψ ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c
Theorem	selberg2lem 23458*	Lemma for selberg2 23459. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( log ` n ) ) - ( (ψ ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1)
Theorem	selberg2 23459*	Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
|- ( x e. RR+ |-> ( ( ( ( (ψ ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selberg2b 23460*	Convert eventual boundedness in selberg2 23459 to boundedness on any interval [ A , +oo ). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 25-May-2016.)
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( ( (ψ ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c
Theorem	chpdifbndlem1 23461*	Lemma for chpdifbnd 23463. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> 1 <_ A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( (ψ ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( (Λ ` m ) x. (ψ ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B )   &    |- C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )   &    |- ( ph -> X e. ( 1 (,) +oo ) )   &    |- ( ph -> Y e. ( X [,] ( A x. X ) ) )   =>    |- ( ph -> ( (ψ ` Y ) - (ψ ` X ) ) <_ ( ( 2 x. ( Y - X ) ) + ( C x. ( X / ( log ` X ) ) ) ) )
Theorem	chpdifbndlem2 23462*	Lemma for chpdifbnd 23463. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> 1 <_ A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( (ψ ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( (Λ ` m ) x. (ψ ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B )   &    |- C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )   =>    |- ( ph -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) )
Theorem	chpdifbnd 23463*	A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) )
Theorem	logdivbnd 23464*	A bound on a sum of logs, used in pntlemk 23514. This is not as precise as logdivsum 23441 in its asymptotic behavior, but it is valid for all N and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` N ) + 1 ) ^ 2 ) / 2 ) )
Theorem	selberg3lem1 23465*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 23459 (written here as sum_ n <_ x , Λ ( n )ψ ( x / n )). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( (Λ ` k ) x. ( log ` k ) ) - ( (ψ ` y ) x. ( log ` y ) ) ) / y ) ) <_ A )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) ) / x ) ) e. O(1) )
Theorem	selberg3lem2 23466*	Lemma for selberg3 23467. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) ) / x ) ) e. O(1)
Theorem	selberg3 23467*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 23459 (written here as sum_ n <_ x , Λ ( n )ψ ( x / n )). Equation 10.6.7 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( (ψ ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. (ψ ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selberg4lem1 23468*	Lemma for selberg4 23469. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )
Theorem	selberg4 23469*	The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form sum_ i j k <_ x , Λ ( i )Λ ( j )Λ ( k ); we eliminate one of the nested sums by using the definition of ψ ( x ) = sum_ k <_ x , Λ ( k ). This statement can thus equivalently be written ψ ( x ) log ^ 2 ( x ) = 2 sum_ i j k <_ x , Λ ( i )Λ ( j )Λ ( k ) + O ( x log x ). Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( (ψ ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. (ψ ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)
Theorem	pntrval 23470*	Define the residual of the second Chebyshev function. The goal is to have R ( x ) e. o ( x ), or R ( x ) / x ~~> r 0. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( A e. RR+ -> ( R ` A ) = ( (ψ ` A ) - A ) )
Theorem	pntrf 23471	Functionality of the residual. Lemma for pnt 23522. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- R : RR+ --> RR
Theorem	pntrmax 23472*	There is a bound on the residual valid for all x. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- E. c e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ c
Theorem	pntrsumo1 23473*	A bound on a sum over R. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1)
Theorem	pntrsumbnd 23474*	A bound on a sum over R. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- E. c e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c
Theorem	pntrsumbnd2 23475*	A bound on a sum over R. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c
Theorem	selbergr 23476*	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.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. RR+ |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( (Λ ` d ) x. ( R ` ( x / d ) ) ) ) / x ) ) e. O(1)
Theorem	selberg3r 23477*	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.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. O(1)
Theorem	selberg4r 23478*	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.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)
Theorem	selberg34r 23479*	The sum of selberg3r 23477 and selberg4r 23478. (Contributed by Mario Carneiro, 31-May-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) - ( (Λ ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1)
Theorem	pntsval 23480*	Define the "Selberg function", whose asymptotic behavior is the content of selberg 23456. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   =>    |- ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( (Λ ` n ) x. ( ( log ` n ) + (ψ ` ( A / n ) ) ) ) )
Theorem	pntsf 23481*	Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   =>    |- S : RR --> RR
Theorem	selbergs 23482*	Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   =>    |- ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
Theorem	selbergsb 23483*	Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   =>    |- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c
Theorem	pntsval2 23484*	The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   =>    |- ( A e. RR -> ( S ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
Theorem	pntrlog2bndlem1 23485*	The sum of selberg3r 23477 and selberg4r 23478. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1)
Theorem	pntrlog2bndlem2 23486*	Lemma for pntrlog2bnd 23492. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. y e. RR+ (ψ ` y ) <_ ( A x. y ) )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
Theorem	pntrlog2bndlem3 23487*	Lemma for pntrlog2bnd 23492. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
Theorem	pntrlog2bndlem4 23488*	Lemma for pntrlog2bnd 23492. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )   =>    |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1)
Theorem	pntrlog2bndlem5 23489*	Lemma for pntrlog2bnd 23492. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) )
Theorem	pntrlog2bndlem6a 23490*	Lemma for pntrlog2bndlem6 23491. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   =>    |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( ( 1 ... ( |_ ` ( x / A ) ) ) u. ( ( ( |_ ` ( x / A ) ) + 1 ) ... ( |_ ` x ) ) ) )
Theorem	pntrlog2bndlem6 23491*	Lemma for pntrlog2bnd 23492. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )   &    |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) )
Theorem	pntrlog2bnd 23492*	A bound on R ( x ) log ^ 2 ( x ). Equation 10.6.15 of [Shapiro], p. 431. (Contributed by Mario Carneiro, 1-Jun-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- ( ( A e. RR /\ 1 <_ A ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` ( x / A ) ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) <_ c )
Theorem	pntpbnd1a 23493*	Lemma for pntpbnd 23496. (Contributed by Mario Carneiro, 11-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- X = ( exp ` ( 2 / E ) )   &    |- ( ph -> Y e. ( X (,) +oo ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( Y < N /\ N <_ ( K x. Y ) ) )   &    |- ( ph -> ( abs ` ( R ` N ) ) <_ ( abs ` ( ( R ` ( N + 1 ) ) - ( R ` N ) ) ) )   =>    |- ( ph -> ( abs ` ( ( R ` N ) / N ) ) <_ E )
Theorem	pntpbnd1 23494*	Lemma for pntpbnd 23496. (Contributed by Mario Carneiro, 11-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- X = ( exp ` ( 2 / E ) )   &    |- ( ph -> Y e. ( X (,) +oo ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )   &    |- C = ( A + 2 )   &    |- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )   &    |- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )   =>    |- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )
Theorem	pntpbnd2 23495*	Lemma for pntpbnd 23496. (Contributed by Mario Carneiro, 11-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- X = ( exp ` ( 2 / E ) )   &    |- ( ph -> Y e. ( X (,) +oo ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )   &    |- C = ( A + 2 )   &    |- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )   &    |- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )   =>    |- -. ph
Theorem	pntpbnd 23496*	Lemma for pnt 23522. Establish smallness of R at a point. Lemma 10.6.1 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e )
Theorem	pntibndlem1 23497	Lemma for pntibnd 23501. (Contributed by Mario Carneiro, 10-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- L = ( ( 1 / 4 ) / ( A + 3 ) )   =>    |- ( ph -> L e. ( 0 (,) 1 ) )
Theorem	pntibndlem2a 23498*	Lemma for pntibndlem2 23499. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- L = ( ( 1 / 4 ) / ( A + 3 ) )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- ( ph -> B e. RR+ )   &    |- K = ( exp ` ( B / ( E / 2 ) ) )   &    |- C = ( ( 2 x. B ) + ( log ` 2 ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- ( ph -> Z e. RR+ )   &    |- ( ph -> N e. NN )   =>    |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )
Theorem	pntibndlem2 23499*	Lemma for pntibnd 23501. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- L = ( ( 1 / 4 ) / ( A + 3 ) )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- ( ph -> B e. RR+ )   &    |- K = ( exp ` ( B / ( E / 2 ) ) )   &    |- C = ( ( 2 x. B ) + ( log ` 2 ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- ( ph -> Z e. RR+ )   &    |- ( ph -> N e. NN )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )   &    |- X = ( ( exp ` ( T / ( E / 4 ) ) ) + Z )   &    |- ( ph -> M e. ( ( exp ` ( C / E ) ) [,) +oo ) )   &    |- ( ph -> Y e. ( X (,) +oo ) )   &    |- ( ph -> ( ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) /\ ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) ) )   =>    |- ( ph -> E. z e. RR+ ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
Theorem	pntibndlem3 23500*	Lemma for pntibnd 23501. Package up pntibndlem2 23499 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- L = ( ( 1 / 4 ) / ( A + 3 ) )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- ( ph -> B e. RR+ )   &    |- K = ( exp ` ( B / ( E / 2 ) ) )   &    |- C = ( ( 2 x. B ) + ( log ` 2 ) )   &    |- ( ph -> E e. ( 0 (,) 1 ) )   &    |- ( ph -> Z e. RR+ )   &    |- ( ph -> A. m e. ( K [,) +oo ) A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) )   =>    |- ( ph -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )