HomeHome Metamath Proof Explorer
Theorem List (p. 208 of 328)
< 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-21514)
  Hilbert Space Explorer  Hilbert Space Explorer
(21515-23037)
  Users' Mathboxes  Users' Mathboxes
(23038-32776)
 

Theorem List for Metamath Proof Explorer - 20701-20800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmulog2sumlem3 20701* Lemma for mulog2sum 20702. (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 20702* 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 20703* 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 20704* 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 20705* Lemma for 2vmadivsum 20706. (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 20706* 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 20707* 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 20708* The Möbius inverse of logsqvma 20707. 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 20709* 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 20710* Lemma for selberg 20713. Estimation of the asymptotic part of selberglem3 20712. (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 20711* Lemma for selberg 20713. (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 20712* Lemma for selberg 20713. Estimation of the left-hand side of logsqvma2 20708. (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 20713* 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 20714* Convert eventual boundedness in selberg 20713 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 20715* Lemma for selberg2 20716. 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 20716* 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 20717* Convert eventual boundedness in selberg2 20716 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 20718* Lemma for chpdifbnd 20720. (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 20719* Lemma for chpdifbnd 20720. (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 20720* 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 20721* A bound on a sum of logs, used in pntlemk 20771. This is not as precise as logdivsum 20698 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 20722* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20716 (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 20723* Lemma for selberg3 20724. 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 20724* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20716 (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 20725* Lemma for selberg4 20726. 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 20726* 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 20727* 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 20728 Functionality of the residual. Lemma for pnt 20779. (Contributed by Mario Carneiro, 8-Apr-2016.)
 |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a
 ) )   =>    |-  R : RR+ --> RR
 
Theorempntrmax 20729* 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 20730* 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 20731* 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 20732* 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 20733* 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 20734* 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 20735* 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 20736* The sum of selberg3r 20734 and selberg4r 20735. (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 20737* Define the "Selberg function", whose asymptotic behavior is the content of selberg 20713. (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 20738* 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 20739* 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 20740* 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 20741* 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 20742* The sum of selberg3r 20734 and selberg4r 20735. (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 20743* Lemma for pntrlog2bnd 20749. 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 20744* Lemma for pntrlog2bnd 20749. 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 20745* Lemma for pntrlog2bnd 20749. 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 20746* Lemma for pntrlog2bnd 20749. 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 20747* Lemma for pntrlog2bndlem6 20748. (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 20748* Lemma for pntrlog2bnd 20749. 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 20749* 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 20750* Lemma for pntpbnd 20753. (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 20751* Lemma for pntpbnd 20753. (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 20752* Lemma for pntpbnd 20753. (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 20753* Lemma for pnt 20779. 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 20754 Lemma for pntibnd 20758. (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 20755* Lemma for pntibndlem2 20756. (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 20756* Lemma for pntibnd 20758. 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 20757* Lemma for pntibnd 20758. Package up pntibndlem2 20756 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 20758* Lemma for pnt 20779. 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 20759 Lemma for pnt 20779. 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 20760* Lemma for pnt 20779. 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 20761* Lemma for pnt 20779. 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 20762* Lemma for pnt 20779. 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 20763* Lemma for pnt 20779. 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 20764* Lemma for pnt 20779. 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 20765* Lemma for pnt 20779. 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 20766* Lemma for pntlemj 20768. (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 20767* Lemma for pntlemj 20768. (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 20768* Lemma for pnt 20779. The induction step. Using pntibnd 20758, 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 20769* Lemma for pnt 20779. Eliminate some assumptions from pntlemj 20768. (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 20770* Lemma for pnt 20779. Add up the pieces in pntlemi 20769 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 20771* Lemma for pnt 20779. 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 20772* Lemma for pnt 20779. 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 20773* Lemma for pnt 20779. Package up pntlemo 20772 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 20774* Lemma for pnt 20779. 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 20775* Lemma for pnt 20779. 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 ) ) ) )
 
Theorempntleml 20776* Lemma for pnt 20779. 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 )
 
Theorempnt3 20777 The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to  x. (Contributed by Mario Carneiro, 1-Jun-2016.)
 |-  ( x  e.  RR+  |->  ( (ψ `  x )  /  x ) )  ~~> r  1
 
Theorempnt2 20778 The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to  x. (Contributed by Mario Carneiro, 1-Jun-2016.)
 |-  ( x  e.  RR+  |->  ( ( theta `  x )  /  x ) )  ~~> r  1
 
Theorempnt 20779 The Prime Number Theorem: the number of prime numbers less than  x tends asymptotically to  x  /  log (
x ) as  x goes to infinity. (Contributed by Mario Carneiro, 1-Jun-2016.)
 |-  ( x  e.  (
 1 (,)  +oo )  |->  ( (π `  x )  /  ( x  /  ( log `  x ) ) ) )  ~~> r  1
 
13.4.13  Ostrowski's theorem
 
Theoremabvcxp 20780* Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  A  =  (AbsVal `  R )   &    |-  B  =  ( Base `  R )   &    |-  G  =  ( x  e.  B  |->  ( ( F `  x )  ^ c  S ) )   =>    |-  ( ( F  e.  A  /\  S  e.  (
 0 (,] 1 ) ) 
 ->  G  e.  A )
 
Theorempadicfval 20781* Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   =>    |-  ( P  e.  Prime  ->  ( J `  P )  =  ( x  e. 
 QQ  |->  if ( x  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  x ) ) ) ) )
 
Theorempadicval 20782* Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   =>    |-  ( ( P  e.  Prime  /\  X  e.  QQ )  ->  ( ( J `
  P ) `  X )  =  if ( X  =  0 ,  0 ,  ( P ^ -u ( P  pCnt  X ) ) ) )
 
Theoremostth2lem1 20783* Lemma for ostth2 20802, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 20802. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, 
n  e.  o ( A ^ n ) for any 
1  <  A. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  (
 ( ph  /\  n  e. 
 NN )  ->  ( A ^ n )  <_  ( n  x.  B ) )   =>    |-  ( ph  ->  A  <_  1 )
 
Theoremqrngbas 20784 The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |- 
 QQ  =  ( Base `  Q )
 
Theoremqdrng 20785 The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  Q  e.  DivRing
 
Theoremqrng0 20786 The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  0  =  ( 0g
 `  Q )
 
Theoremqrng1 20787 The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  1  =  ( 1r
 `  Q )
 
Theoremqrngneg 20788 The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  ( X  e.  QQ  ->  ( ( inv g `  Q ) `  X )  =  -u X )
 
Theoremqrngdiv 20789 The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  ( ( X  e.  QQ  /\  Y  e.  QQ  /\  Y  =/=  0 ) 
 ->  ( X (/r `  Q ) Y )  =  ( X  /  Y ) )
 
Theoremqabvle 20790 By using induction on  N, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   =>    |-  ( ( F  e.  A  /\  N  e.  NN0 )  ->  ( F `  N )  <_  N )
 
Theoremqabvexp 20791 Induct the product rule abvmul 15610 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   =>    |-  ( ( F  e.  A  /\  M  e.  QQ  /\  N  e.  NN0 )  ->  ( F `  ( M ^ N ) )  =  ( ( F `
  M ) ^ N ) )
 
Theoremostthlem1 20792* Lemma for ostth 20804. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  ( ph  ->  F  e.  A )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ( ph  /\  n  e.  ( ZZ>= `  2 )
 )  ->  ( F `  n )  =  ( G `  n ) )   =>    |-  ( ph  ->  F  =  G )
 
Theoremostthlem2 20793* Lemma for ostth 20804. Refine ostthlem1 20792 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  ( ph  ->  F  e.  A )   &    |-  ( ph  ->  G  e.  A )   &    |-  ( ( ph  /\  p  e.  Prime )  ->  ( F `  p )  =  ( G `  p ) )   =>    |-  ( ph  ->  F  =  G )
 
Theoremqabsabv 20794 The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   =>    |-  ( abs  |`  QQ )  e.  A
 
Theorempadicabv 20795* The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  F  =  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  ( N ^ ( P  pCnt  x ) ) ) )   =>    |-  ( ( P  e.  Prime  /\  N  e.  (
 0 (,) 1 ) ) 
 ->  F  e.  A )
 
Theorempadicabvf 20796* The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   =>    |-  J : Prime --> A
 
Theorempadicabvcxp 20797* All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   =>    |-  ( ( P  e.  Prime  /\  R  e.  RR+ )  ->  ( y  e. 
 QQ  |->  ( ( ( J `  P ) `
  y )  ^ c  R ) )  e.  A )
 
Theoremostth1 20798* - Lemma for ostth 20804: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If  F is equal to  1 on the primes, then by complete induction and the multiplicative property abvmul 15610 of the absolute value,  F is equal to  1 on all the integers, and ostthlem1 20792 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   &    |-  K  =  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  1 ) )   &    |-  ( ph  ->  F  e.  A )   &    |-  ( ph  ->  A. n  e.  NN  -.  1  <  ( F `
  n ) )   &    |-  ( ph  ->  A. n  e. 
 Prime  -.  ( F `  n )  <  1 )   =>    |-  ( ph  ->  F  =  K )
 
Theoremostth2lem2 20799* Lemma for ostth2 20802. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   &    |-  K  =  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  1 ) )   &    |-  ( ph  ->  F  e.  A )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  2 ) )   &    |-  ( ph  ->  1  <  ( F `  N ) )   &    |-  R  =  ( ( log `  ( F `  N ) ) 
 /  ( log `  N ) )   &    |-  ( ph  ->  M  e.  ( ZZ>= `  2
 ) )   &    |-  S  =  ( ( log `  ( F `  M ) ) 
 /  ( log `  M ) )   &    |-  T  =  if ( ( F `  M )  <_  1 ,  1 ,  ( F `
  M ) )   =>    |-  ( ( ph  /\  X  e.  NN0  /\  Y  e.  ( 0 ... (
 ( M ^ X )  -  1 ) ) )  ->  ( F `  Y )  <_  (
 ( M  x.  X )  x.  ( T ^ X ) ) )
 
Theoremostth2lem3 20800* Lemma for ostth2 20802. (Contributed by Mario Carneiro, 10-Sep-2014.)
 |-  Q  =  (flds  QQ )   &    |-  A  =  (AbsVal `  Q )   &    |-  J  =  ( q  e.  Prime  |->  ( x  e.  QQ  |->  if ( x  =  0 , 
 0 ,  ( q ^ -u ( q  pCnt  x ) ) ) ) )   &    |-  K  =  ( x  e.  QQ  |->  if ( x  =  0 ,  0 ,  1 ) )   &    |-  ( ph  ->  F  e.  A )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  2 ) )   &    |-  ( ph  ->  1  <  ( F `  N ) )   &    |-  R  =  ( ( log `  ( F `  N ) ) 
 /  ( log `  N ) )   &    |-  ( ph  ->  M  e.  ( ZZ>= `  2
 ) )   &    |-  S  =  ( ( log `  ( F `  M ) ) 
 /  ( log `  M ) )   &    |-  T  =  if ( ( F `  M )  <_  1 ,  1 ,  ( F `
  M ) )   &    |-  U  =  ( ( log `  N )  /  ( log `  M )
 )   =>    |-  ( ( ph  /\  X  e.  NN )  ->  (
 ( ( F `  N )  /  ( T  ^ c  U ) ) ^ X ) 
 <_  ( X  x.  (
 ( M  x.  T )  x.  ( U  +  1 ) ) ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113