P. 239 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chpo1ub 23801	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.)
|- ( x e. RR+ |-> ( (ψ ` x ) / x ) ) e. O(1)
Theorem	chpo1ubb 23802*	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.)
|- E. c e. RR+ A. x e. RR+ (ψ ` x ) <_ ( c x. x )
Theorem	vmadivsum 23803*	The sum of the von Mangoldt function over n is asymptotic to log x + O(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.)
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O(1)
Theorem	vmadivsumb 23804*	Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.)
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) <_ c
Theorem	rplogsumlem1 23805*	Lemma for rplogsum 23848. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ 2 )
Theorem	rplogsumlem2 23806*	Lemma for rplogsum 23848. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( A e. ZZ -> sum_ n e. ( 1 ... A ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) <_ 2 )
Theorem	dchrisum0lem1a 23807	Lemma for dchrisum0lem1 23837. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X <_ ( ( X ^ 2 ) / D ) /\ ( |_ ` ( ( X ^ 2 ) / D ) ) e. ( ZZ>= ` ( |_ ` X ) ) ) )
Theorem	rpvmasumlem 23808*	Lemma for rpvmasum 23847. Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n )Λ ( n ) / n ) = log x + O(1), where .1. ( x ) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.)
|- Z = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> N e. NN )   &    |- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   =>    |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( (Λ ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )
Theorem	dchrisumlema 23809*	Lemma for dchrisum 23813. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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. )   &    |- ( n = x -> A = B )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ n e. RR+ ) -> A e. RR )   &    |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )   &    |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )   &    |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )   =>    |- ( ph -> ( ( I e. RR+ -> [_ I / n ]_ A e. RR ) /\ ( I e. ( M [,) +oo ) -> 0 <_ [_ I / n ]_ A ) ) )
Theorem	dchrisumlem1 23810*	Lemma for dchrisum 23813. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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. )   &    |- ( n = x -> A = B )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ n e. RR+ ) -> A e. RR )   &    |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )   &    |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )   &    |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )   &    |- ( ph -> R e. RR )   &    |- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )   =>    |- ( ( ph /\ U e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ U ) ( X ` ( L ` n ) ) ) <_ R )
Theorem	dchrisumlem2 23811*	Lemma for dchrisum 23813. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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. )   &    |- ( n = x -> A = B )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ n e. RR+ ) -> A e. RR )   &    |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )   &    |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )   &    |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )   &    |- ( ph -> R e. RR )   &    |- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> M <_ U )   &    |- ( ph -> U <_ ( I + 1 ) )   &    |- ( ph -> I e. NN )   &    |- ( ph -> J e. ( ZZ>= ` I ) )   =>    |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
Theorem	dchrisumlem3 23812*	Lemma for dchrisum 23813. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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. )   &    |- ( n = x -> A = B )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ n e. RR+ ) -> A e. RR )   &    |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )   &    |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )   &    |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )   &    |- ( ph -> R e. RR )   &    |- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )   =>    |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
Theorem	dchrisum 23813*	If n e. [ M , +oo ) |-> A ( n ) is a positive decreasing function approaching zero, then the infinite sum sum_ n , X ( n ) A ( n ) is convergent, with the partial sum sum_ n <_ x , X ( n ) A ( n ) within O ( A ( M ) ) of the limit T. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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. )   &    |- ( n = x -> A = B )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ n e. RR+ ) -> A e. RR )   &    |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )   &    |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )   &    |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )   =>    |- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. x e. ( M [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. B ) ) )
Theorem	dchrmusumlema 23814*	Lemma for dchrmusum 23845 and dchrisumn0 23842. Apply dchrisum 23813 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 23815*	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 23816*	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 23817*	Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n )Λ ( n ) / n ) given in dchrvmasumlem1 23816. 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 23818*	Combine the results of dchrvmasumlem1 23816 and dchrvmasum2lem 23817 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 23819*	Lemma for dchrvmasum 23846. (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 23820*	Lemma for dchrvmasum 23846. (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 23821*	Lemma for dchrvmasum 23846 and dchrvmasumif 23824. Apply dchrisum 23813 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 23822*	Lemma for dchrvmasumif 23824. (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 23823*	Lemma for dchrvmasum 23846. (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 23824*	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 23846.) (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 23825*	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 23826*	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 23827*	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 23828*	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 23829*	Lemma for dchrisum0flb 23831. 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 23830*	Lemma for dchrisum0flb 23831. 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 23831*	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 23832*	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 23833*	A partial result along the lines of rpvmasum 23847. 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 23834*	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 23835*	Lemma for dchrisum0 23841. Apply dchrisum 23813 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 23836*	Lemma for dchrisum0lem1 23837. (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 23837*	Lemma for dchrisum0 23841. (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 23838*	Lemma for dchrisum0 23841. (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 23839*	Lemma for dchrisum0 23841. (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 23840*	Lemma for dchrisum0 23841. (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 23841*	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 23815 and dchrvmasumif 23824. 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 23842*	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 23815 and dchrvmasumif 23824. 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 23843*	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 23844*	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 23845*	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 23846*	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 23847*	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 23848*	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 23849	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 23850*	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 23851*	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 23852*	Lemma for mulogsum 23853. (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 23853*	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 23854*	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 23855*	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 23856*	Lemma for mulog2sum 23858. (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 23857*	Lemma for mulog2sum 23858. (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 23858*	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 23859*	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 23860*	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 23861*	Lemma for 2vmadivsum 23862. (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 23862*	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 23863*	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 23864*	The Möbius inverse of logsqvma 23863. 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 23865*	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 23866*	Lemma for selberg 23869. Estimation of the asymptotic part of selberglem3 23868. (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 23867*	Lemma for selberg 23869. (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 23868*	Lemma for selberg 23869. Estimation of the left-hand side of logsqvma2 23864. (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 23869*	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 23870*	Convert eventual boundedness in selberg 23869 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 23871*	Lemma for selberg2 23872. 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 23872*	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 23873*	Convert eventual boundedness in selberg2 23872 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 23874*	Lemma for chpdifbnd 23876. (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 23875*	Lemma for chpdifbnd 23876. (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 23876*	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 23877*	A bound on a sum of logs, used in pntlemk 23927. This is not as precise as logdivsum 23854 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 23878*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 23872 (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 23879*	Lemma for selberg3 23880. 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 23880*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 23872 (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 23881*	Lemma for selberg4 23882. 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 23882*	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 23883*	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 23884	Functionality of the residual. Lemma for pnt 23935. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- R : RR+ --> RR
Theorem	pntrmax 23885*	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 23886*	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 23887*	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 23888*	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 23889*	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 23890*	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 23891*	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 23892*	The sum of selberg3r 23890 and selberg4r 23891. (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 23893*	Define the "Selberg function", whose asymptotic behavior is the content of selberg 23869. (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 23894*	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 23895*	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 23896*	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 23897*	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 23898*	The sum of selberg3r 23890 and selberg4r 23891. (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 23899*	Lemma for pntrlog2bnd 23905. 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 23900*	Lemma for pntrlog2bnd 23905. 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) )