P. 253 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25201-25300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rpvmasum2 25201*	A partial result along the lines of rpvmasum 25215. 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 25202*	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 25203*	Lemma for dchrisum0 25209. Apply dchrisum 25181 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 25204*	Lemma for dchrisum0lem1 25205. (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 25205*	Lemma for dchrisum0 25209. (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 25206*	Lemma for dchrisum0 25209. (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 25207*	Lemma for dchrisum0 25209. (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 25208*	Lemma for dchrisum0 25209. (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 25209*	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 25183 and dchrvmasumif 25192. 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 25210*	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 25183 and dchrvmasumif 25192. 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 25211*	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 25212*	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 25213*	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 25214*	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 25215*	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 25216*	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 25217	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 25218*	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.13  The Prime Number Theorem
Theorem	mudivsum 25219*	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 25220*	Lemma for mulogsum 25221. (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 25221*	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 25222*	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 25223*	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 25224*	Lemma for mulog2sum 25226. (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 25225*	Lemma for mulog2sum 25226. (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 25226*	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 25227*	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 25228*	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 25229*	Lemma for 2vmadivsum 25230. (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 25230*	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 25231*	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 25232*	The Möbius inverse of logsqvma 25231. 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 25233*	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 25234*	Lemma for selberg 25237. Estimation of the asymptotic part of selberglem3 25236. (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 25235*	Lemma for selberg 25237. (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 25236*	Lemma for selberg 25237. Estimation of the left-hand side of logsqvma2 25232. (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 25237*	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 25238*	Convert eventual boundedness in selberg 25237 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 25239*	Lemma for selberg2 25240. 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 25240*	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 25241*	Convert eventual boundedness in selberg2 25240 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 25242*	Lemma for chpdifbnd 25244. (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 25243*	Lemma for chpdifbnd 25244. (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 25244*	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 25245*	A bound on a sum of logs, used in pntlemk 25295. This is not as precise as logdivsum 25222 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 25246*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 25240 (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 25247*	Lemma for selberg3 25248. 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 25248*	Introduce a log weighting on the summands of sum_ m x. n <_ x , Λ ( m )Λ ( n ), the core of selberg2 25240 (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 25249*	Lemma for selberg4 25250. 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 25250*	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 25251*	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 25252	Functionality of the residual. Lemma for pnt 25303. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- R : RR+ --> RR
Theorem	pntrmax 25253*	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 25254*	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 25255*	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 25256*	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 25257*	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 25258*	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 25259*	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 25260*	The sum of selberg3r 25258 and selberg4r 25259. (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 25261*	Define the "Selberg function", whose asymptotic behavior is the content of selberg 25237. (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 25262*	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 25263*	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 25264*	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 25265*	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 25266*	The sum of selberg3r 25258 and selberg4r 25259. (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 25267*	Lemma for pntrlog2bnd 25273. 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 25268*	Lemma for pntrlog2bnd 25273. 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 25269*	Lemma for pntrlog2bnd 25273. 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 25270*	Lemma for pntrlog2bnd 25273. 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 25271*	Lemma for pntrlog2bndlem6 25272. (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 25272*	Lemma for pntrlog2bnd 25273. 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 25273*	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 25274*	Lemma for pntpbnd 25277. (Contributed by Mario Carneiro, 11-Apr-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.)
|- 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 25275*	Lemma for pntpbnd 25277. (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 25276*	Lemma for pntpbnd 25277. (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 25277*	Lemma for pnt 25303. 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 25278	Lemma for pntibnd 25282. (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 25279*	Lemma for pntibndlem2 25280. (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 25280*	Lemma for pntibnd 25282. 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 25281*	Lemma for pntibnd 25282. Package up pntibndlem2 25280 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 ) )
Theorem	pntibnd 25282*	Lemma for pnt 25303. Establish smallness of R on an interval. Lemma 10.6.2 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   =>    |- E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) 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 )
Theorem	pntlemd 25283	Lemma for pnt 25303. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, A is C^*, B is c1, L is λ, D is c2, and F is c3. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   =>    |- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
Theorem	pntlemc 25284*	Lemma for pnt 25303. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, U is α, E is ε, and K is K. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   =>    |- ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
Theorem	pntlema 25285*	Lemma for pnt 25303. Closure for the constants used in the proof. The mammoth expression W is a number large enough to satisfy all the lower bounds needed for Z. For comparison with Equation 10.6.27 of [Shapiro], p. 434, Y is x2, X is x1, C is the big-O constant in Equation 10.6.29 of [Shapiro], p. 435, and W is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of [Shapiro], p. 436. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   =>    |- ( ph -> W e. RR+ )
Theorem	pntlemb 25286*	Lemma for pnt 25303. Unpack all the lower bounds contained in W, in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, Z is x. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   =>    |- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqr ` Z ) /\ ( sqr ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqr ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / (; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
Theorem	pntlemg 25287*	Lemma for pnt 25303. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, M is j^* and N is ĵ. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   =>    |- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
Theorem	pntlemh 25288*	Lemma for pnt 25303. Bounds on the subintervals in the induction. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   =>    |- ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqr ` Z ) ) )
Theorem	pntlemn 25289*	Lemma for pnt 25303. The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   =>    |- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) x. ( log ` J ) ) )
Theorem	pntlemq 25290*	Lemma for pntlemj 25292. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   &    |- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )   &    |- ( ph -> V e. RR+ )   &    |- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )   &    |- ( ph -> J e. ( M..^ N ) )   &    |- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )   =>    |- ( ph -> I C_ O )
Theorem	pntlemr 25291*	Lemma for pntlemj 25292. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   &    |- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )   &    |- ( ph -> V e. RR+ )   &    |- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )   &    |- ( ph -> J e. ( M..^ N ) )   &    |- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )   =>    |- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
Theorem	pntlemj 25292*	Lemma for pnt 25303. The induction step. Using pntibnd 25282, we find an interval in K ^ J ... K ^ ( J + 1 ) which is sufficiently large and has a much smaller value, R ( z ) / z <_ E (instead of our original bound R ( z ) / z <_ U). (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   &    |- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )   &    |- ( ph -> V e. RR+ )   &    |- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )   &    |- ( ph -> J e. ( M..^ N ) )   &    |- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )   =>    |- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
Theorem	pntlemi 25293*	Lemma for pnt 25303. Eliminate some assumptions from pntlemj 25292. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   &    |- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )   =>    |- ( ( ph /\ J e. ( M..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
Theorem	pntlemf 25294*	Lemma for pnt 25303. Add up the pieces in pntlemi 25293 to get an estimate slightly better than the naive lower bound 0. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   =>    |- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / (; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
Theorem	pntlemk 25295*	Lemma for pnt 25303. Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   =>    |- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )
Theorem	pntlemo 25296*	Lemma for pnt 25303. Combine all the estimates to establish a smaller eventual bound on R ( Z ) / Z. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> Z e. ( W [,) +oo ) )   &    |- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )   &    |- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> 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 ) )   &    |- ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )   =>    |- ( ph -> ( abs ` ( ( R ` Z ) / Z ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
Theorem	pntleme 25297*	Lemma for pnt 25303. Package up pntlemo 25296 in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> ( X e. RR+ /\ Y < X ) )   &    |- ( ph -> C e. RR+ )   &    |- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( (; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   &    |- ( ph -> A. k e. ( K [,) +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 ) )   &    |- ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )   =>    |- ( ph -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
Theorem	pntlem3 25298*	Lemma for pnt 25303. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) (Proof shortened by AV, 27-Sep-2020.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- T = { t e. ( 0 [,] A ) | E. y e. RR+ A. z e. ( y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ t }   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ u e. T ) -> ( u - ( C x. ( u ^ 3 ) ) ) e. T )   =>    |- ( ph -> ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1 )
Theorem	pntlemp 25299*	Lemma for pnt 25303. Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / 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 ) )   &    |- ( ph -> U e. RR+ )   &    |- ( ph -> U <_ A )   &    |- E = ( U / D )   &    |- K = ( exp ` ( B / E ) )   &    |- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )   &    |- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )   =>    |- ( ph -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
Theorem	pntleml 25300*	Lemma for pnt 25303. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> L e. ( 0 (,) 1 ) )   &    |- D = ( A + 1 )   &    |- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / (; 3 2 x. B ) ) / ( D ^ 2 ) ) )   &    |- ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / 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 ) )   =>    |- ( ph -> ( x e. RR+ |-> ( (ψ ` x ) / x ) ) ~~> r 1 )