HomeHome Metamath Proof Explorer
Theorem List (p. 206 of 311)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

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

Theorem List for Metamath Proof Explorer - 20501-20600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdchrisum0 20501* 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 20475 and dchrvmasumif 20484. 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
 
Theoremdchrisumn0 20502* 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 20475 and dchrvmasumif 20484. 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 )
 
Theoremdchrmusumlem 20503* 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 ) )
 
Theoremdchrvmasumlem 20504* 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 ) )
 
Theoremdchrmusum 20505* 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 ) )
 
Theoremdchrvmasum 20506* 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 ) )
 
Theoremrpvmasum 20507* 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 ) )
 
Theoremrplogsum 20508* 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 ) )
 
Theoremdirith2 20509 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 )
 
Theoremdirith 20510* 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. (Contributed by Mario Carneiro, 12-May-2016.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  { p  e.  Prime  |  N  ||  ( p  -  A ) }  ~~  NN )
 
13.4.12  The Prime Number Theorem
 
Theoremmudivsum 20511* 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 )
 
Theoremmulogsumlem 20512* Lemma for mulogsum 20513. (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 )
 
Theoremmulogsum 20513* 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 )
 
Theoremlogdivsum 20514* 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 ) ) )
 
Theoremmulog2sumlem1 20515* 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 ) ) )
 
Theoremmulog2sumlem2 20516* Lemma for mulog2sum 20518. (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 ) )
 
Theoremmulog2sumlem3 20517* Lemma for mulog2sum 20518. (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 ) )
 
Theoremmulog2sum 20518* 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 )
 
Theoremvmalogdivsum2 20519* 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 )
 
Theoremvmalogdivsum 20520* 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 )
 
Theorem2vmadivsumlem 20521* Lemma for 2vmadivsum 20522. (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 ) )
 
Theorem2vmadivsum 20522* 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 )
 
Theoremlogsqvma 20523* 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 ) )
 
Theoremlogsqvma2 20524* The Möbius inverse of logsqvma 20523. 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 ) ) ) )
 
Theoremlog2sumbnd 20525* 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 ) )
 
Theoremselberglem1 20526* Lemma for selberg 20529. Estimation of the asymptotic part of selberglem3 20528. (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 )
 
Theoremselberglem2 20527* Lemma for selberg 20529. (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 )
 
Theoremselberglem3 20528* Lemma for selberg 20529. Estimation of the left hand side of logsqvma2 20524. (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 )
 
Theoremselberg 20529* 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 )
 
Theoremselbergb 20530* Convert eventual boundedness in selberg 20529 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
 
Theoremselberg2lem 20531* Lemma for selberg2 20532. 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 )
 
Theoremselberg2 20532* Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
 |-  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O ( 1 )
 
Theoremselberg2b 20533* Convert eventual boundedness in selberg2 20532 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
 
Theoremchpdifbndlem1 20534* Lemma for chpdifbnd 20536. (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 ) ) ) ) )
 
Theoremchpdifbndlem2 20535* Lemma for chpdifbnd 20536. (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 ) ) ) ) )
 
Theoremchpdifbnd 20536* A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.)
 |-  ( ( 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 ) ) ) ) )
 
Theoremlogdivbnd 20537* A bound on a sum of logs, used in pntlemk 20587. This is not as precise as logdivsum 20514 in its asymptotic behavior, but it is valid for all  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
 ) )
 
Theoremselberg3lem1 20538* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20532 (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 ) )
 
Theoremselberg3lem2 20539* Lemma for selberg3 20540. 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 )
 
Theoremselberg3 20540* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20532 (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 )
 
Theoremselberg4lem1 20541* Lemma for selberg4 20542. 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 ) )
 
Theoremselberg4 20542* The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form  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 )
 
Theorempntrval 20543* 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 ) )
 
Theorempntrf 20544 Functionality of the residual. Lemma for pnt 20595. (Contributed by Mario Carneiro, 8-Apr-2016.)
 |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a
 ) )   =>    |-  R : RR+ --> RR
 
Theorempntrmax 20545* 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
 
Theorempntrsumo1 20546* 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 )
 
Theorempntrsumbnd 20547* 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
 
Theorempntrsumbnd2 20548* 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
 
Theoremselbergr 20549* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.)
 |-  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 )
 
Theoremselberg3r 20550* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  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 )
 
Theoremselberg4r 20551* Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.)
 |-  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 )
 
Theoremselberg34r 20552* The sum of selberg3r 20550 and selberg4r 20551. (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 )
 
Theorempntsval 20553* Define the "Selberg function", whose asymptotic behavior is the content of selberg 20529. (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 ) ) ) ) )
 
Theorempntsf 20554* 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
 
Theoremselbergs 20555* 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 )
 
Theoremselbergsb 20556* 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
 
Theorempntsval2 20557* The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 ) ) ) ) )
 
Theorempntrlog2bndlem1 20558* The sum of selberg3r 20550 and selberg4r 20551. (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 )
 
Theorempntrlog2bndlem2 20559* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 ) )
 
Theorempntrlog2bndlem3 20560* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 ) )
 
Theorempntrlog2bndlem4 20561* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 )
 
Theorempntrlog2bndlem5 20562* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 ) )
 
Theorempntrlog2bndlem6a 20563* Lemma for pntrlog2bndlem6 20564. (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 ) ) ) )
 
Theorempntrlog2bndlem6 20564* Lemma for pntrlog2bnd 20565. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
 |-  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 ) )
 
Theorempntrlog2bnd 20565* 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 )
 
Theorempntpbnd1a 20566* Lemma for pntpbnd 20569. (Contributed by Mario Carneiro, 11-Apr-2016.)
 |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a
 ) )   &    |-  ( ph  ->  E  e.  ( 0 (,) 1 ) )   &    |-  X  =  ( exp `  (
 2  /  E )
 )   &    |-  ( ph  ->  Y  e.  ( X (,)  +oo ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  ( Y  <  N 
 /\  N  <_  ( K  x.  Y ) ) )   &    |-  ( ph  ->  ( abs `  ( R `  N ) )  <_  ( abs `  ( ( R `  ( N  +  1 ) )  -  ( R `  N ) ) ) )   =>    |-  ( ph  ->  ( abs `  ( ( R `  N )  /  N ) )  <_  E )
 
Theorempntpbnd1 20567* Lemma for pntpbnd 20569. (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 )
 
Theorempntpbnd2 20568* Lemma for pntpbnd 20569. (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
 
Theorempntpbnd 20569* Lemma for pnt 20595. 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 )
 
Theorempntibndlem1 20570 Lemma for pntibnd 20574. (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
 ) )
 
Theorempntibndlem2a 20571* Lemma for pntibndlem2 20572. (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 ) ) )
 
Theorempntibndlem2 20572* Lemma for pntibnd 20574. 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 ) )
 
Theorempntibndlem3 20573* Lemma for pntibnd 20574. Package up pntibndlem2 20572 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 ) )
 
Theorempntibnd 20574* Lemma for pnt 20595. 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 )
 
Theorempntlemd 20575 Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434,  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+ ) )
 
Theorempntlemc 20576* Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434,  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+ )
 ) )
 
Theorempntlema 20577* Lemma for pnt 20595. 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+ )
 
Theorempntlemb 20578* Lemma for pnt 20595. 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 ) ) ) ) )
 
Theorempntlemg 20579* Lemma for pnt 20595. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434,  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 ) ) )
 
Theorempntlemh 20580* Lemma for pnt 20595. 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 )
 ) )
 
Theorempntlemn 20581* Lemma for pnt 20595. 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 ) ) )
 
Theorempntlemq 20582* Lemma for pntlemj 20584. (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 )
 
Theorempntlemr 20583* Lemma for pntlemj 20584. (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 ) ) ) ) )
 
Theorempntlemj 20584* Lemma for pnt 20595. The induction step. Using pntibnd 20574, 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 ) ) )
 
Theorempntlemi 20585* Lemma for pnt 20595. Eliminate some assumptions from pntlemj 20584. (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 ) ) )
 
Theorempntlemf 20586* Lemma for pnt 20595. Add up the pieces in pntlemi 20585 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 ) ) )
 
Theorempntlemk 20587* Lemma for pnt 20595. 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 ) ) )
 
Theorempntlemo 20588* Lemma for pnt 20595. 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 ) ) ) )
 
Theorempntleme 20589* Lemma for pnt 20595. Package up pntlemo 20588 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 ) ) ) )
 
Theorempntlem3 20590* Lemma for pnt 20595. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.)
 |-  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 )
 
Theorempntlemp 20591* Lemma for pnt 20595. 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 )   =>