HomeHome Metamath Proof Explorer
Theorem List (p. 208 of 323)
< 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-21500)
  Hilbert Space Explorer  Hilbert Space Explorer
(21501-23023)
  Users' Mathboxes  Users' Mathboxes
(23024-32227)
 

Theorem List for Metamath Proof Explorer - 20701-20800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremselberg2lem 20701* Lemma for selberg2 20702. 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 20702* 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 20703* Convert eventual boundedness in selberg2 20702 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 20704* Lemma for chpdifbnd 20706. (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 20705* Lemma for chpdifbnd 20706. (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 20706* 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 20707* A bound on a sum of logs, used in pntlemk 20757. This is not as precise as logdivsum 20684 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 20708* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20702 (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 20709* Lemma for selberg3 20710. 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 20710* Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20702 (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 20711* Lemma for selberg4 20712. 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 20712* 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 20713* 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 20714 Functionality of the residual. Lemma for pnt 20765. (Contributed by Mario Carneiro, 8-Apr-2016.)
 |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a
 ) )   =>    |-  R : RR+ --> RR
 
Theorempntrmax 20715* 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 20716* 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 20717* 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 20718* 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 20719* 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 20720* 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 20721* 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 20722* The sum of selberg3r 20720 and selberg4r 20721. (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 20723* Define the "Selberg function", whose asymptotic behavior is the content of selberg 20699. (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 20724* 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 20725* 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 20726* 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 20727* 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 20728* The sum of selberg3r 20720 and selberg4r 20721. (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 20729* Lemma for pntrlog2bnd 20735. 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 20730* Lemma for pntrlog2bnd 20735. 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 20731* Lemma for pntrlog2bnd 20735. 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 20732* Lemma for pntrlog2bnd 20735. 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 20733* Lemma for pntrlog2bndlem6 20734. (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 20734* Lemma for pntrlog2bnd 20735. 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 20735* 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 20736* Lemma for pntpbnd 20739. (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 20737* Lemma for pntpbnd 20739. (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 20738* Lemma for pntpbnd 20739. (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 20739* Lemma for pnt 20765. 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 20740 Lemma for pntibnd 20744. (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 20741* Lemma for pntibndlem2 20742. (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 20742* Lemma for pntibnd 20744. 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 20743* Lemma for pntibnd 20744. Package up pntibndlem2 20742 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 20744* Lemma for pnt 20765. 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 20745 Lemma for pnt 20765. 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 20746* Lemma for pnt 20765. 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 20747* Lemma for pnt 20765. 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 20748* Lemma for pnt 20765. 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 20749* Lemma for pnt 20765. 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 20750* Lemma for pnt 20765. 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 20751* Lemma for pnt 20765. 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 20752* Lemma for pntlemj 20754. (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 20753* Lemma for pntlemj 20754. (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 20754* Lemma for pnt 20765. The induction step. Using pntibnd 20744, 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 20755* Lemma for pnt 20765. Eliminate some assumptions from pntlemj 20754. (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 20756* Lemma for pnt 20765. Add up the pieces in pntlemi 20755 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 20757* Lemma for pnt 20765. 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 20758* Lemma for pnt 20765. 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 20759* Lemma for pnt 20765. Package up pntlemo 20758 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 20760* Lemma for pnt 20765. 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 20761* Lemma for pnt 20765. 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 20762* Lemma for pnt 20765. 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 20763 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 20764 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 20765 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 20766* 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 20767* 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 20768* 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 20769* Lemma for ostth2 20788, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 20788. 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 20770 The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |- 
 QQ  =  ( Base `  Q )
 
Theoremqdrng 20771 The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  Q  e.  DivRing
 
Theoremqrng0 20772 The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  0  =  ( 0g
 `  Q )
 
Theoremqrng1 20773 The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
 |-  Q  =  (flds  QQ )   =>    |-  1  =  ( 1r
 `  Q )
 
Theoremqrngneg 20774 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 20775 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 20776 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 20777 Induct the product rule abvmul 15596 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 20778* Lemma for ostth 20790. 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 20779* Lemma for ostth 20790. Refine ostthlem1 20778 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 20780 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 20781* 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 20782* 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 20783* 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 20784* - Lemma for ostth 20790: 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 15596 of the absolute value,  F is equal to  1 on all the integers, and ostthlem1 20778 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 20785* Lemma for ostth2 20788. (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 20786* Lemma for ostth2 20788. (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 ) ) ) )
 
Theoremostth2lem4 20787* Lemma for ostth2 20788. (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  ->  (
 1  <  ( F `  M )  /\  R  <_  S ) )
 
Theoremostth2 20788* - Lemma for ostth 20790: regular case. (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  ->  E. a  e.  ( 0 (,] 1
 ) F  =  ( y  e.  QQ  |->  ( ( abs `  y
 )  ^ c  a ) ) )
 
Theoremostth3 20789* - Lemma for ostth 20790: p-adic case. (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  ->  P  e.  Prime )   &    |-  ( ph  ->  ( F `  P )  <  1 )   &    |-  R  =  -u ( ( log `  ( F `  P ) )  /  ( log `  P ) )   &    |-  S  =  if (
 ( F `  P )  <_  ( F `  p ) ,  ( F `  p ) ,  ( F `  P ) )   =>    |-  ( ph  ->  E. a  e.  RR+  F  =  ( y  e.  QQ  |->  ( ( ( J `  P ) `  y
 )  ^ c  a ) ) )
 
Theoremostth 20790* Ostrowski's theorem, which classifies all absolute values on  QQ. Any such absolute value must either be the trivial absolute value  K, a constant exponent  0  <  a  <_  1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (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 ) )   =>    |-  ( F  e.  A  <->  ( F  =  K  \/  E. a  e.  ( 0 (,] 1 ) F  =  ( y  e. 
 QQ  |->  ( ( abs `  y )  ^ c  a ) )  \/ 
 E. a  e.  RR+  E. g  e.  ran  J  F  =  ( y  e.  QQ  |->  ( ( g `
  y )  ^ c  a ) ) ) )
 
PART 14  GUIDES AND MISCELLANEA
 
14.1  Guides (conventions, explanations, and examples)
 
14.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. Logic and set theory provide a foundation for all of mathematics. To learn about them, you should study one or more of the references listed below. We indicate references using square brackets. The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

  • Axioms of propositional calculus - [Margaris].
  • Axioms of predicate calculus - [Megill] (System S3' in the article referenced).
  • Theorems of propositional calculus - [WhiteheadRussell].
  • Theorems of pure predicate calculus - [Margaris].
  • Theorems of equality and substitution - [Monk2], [Tarski], [Megill].
  • Axioms of set theory - [BellMachover].
  • Development of set theory - [TakeutiZaring]. (The first part of [Quine] has a good explanation of the powerful device of "virtual" or class abstractions, which is essential to our development.)
  • Construction of real and complex numbers - [Gleason]
  • Theorems about real numbers - [Apostol]
 
Theoremconventions 20791 Here are some of the conventions we use in the Metamath Proof Explorer (aka "set.mm"), and how they correspond to typical textbook language (skipping the many cases where they're identical):

  • Notation. Where possible, the notation attempts to conform to modern conventions, with variations due to our choice of the axiom system or to make proofs shorter. However, our notation is strictly sequential (left-to-right). For example, summation is written in the form  sum_ k  e.  A B (df-sum 12161) which denotes that index variable  k ranges over  A when evaluating  B. Thus,  sum_ k  e.  NN  ( 1  /  ( 2 ^ k ) )  =  1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12340). Also, the method of definition, the axioms for predicate calculus, and the development of substitution are somewhat different from those found in standard texts. For example, the expressions for the axioms were designed for direct derivation of standard results without excessive use of metatheorems. (See Theorem 9.7 of [Megill] p. 448 for a rigorous justification.) The notation is usually explained in more detail when first introduced.
  • Axiomatic assertions ($a). All axiomatic assertions ($a statements) starting with "  |-" have labels starting with "ax-" (axioms) or "df-" (definitions). A statement with a label starting with "ax-" corresponds to what is traditionally called an axiom. A statement with a label starting with "df-" introduces new symbols or a new relationship among symbols that can be eliminated; they always extend the definition of a wff or class. Metamath blindly treats $a statements as new given facts but does not try to justify them. The mmj2 program will justify the definitions as sound, except for 4 (df-bi, df-cleq, df-clel, df-clab) that require a more complex metalogical justification by hand.
  • Proven axioms. In some cases we wish to treat an expression as an axiom in later theorems, even though it can be proved. For example, we derive the postulates or axioms of complex arithmetic as theorems of ZFC set theory. For convenience, after deriving the postulates we re-introduce them as new axioms on top of set theory. This lets us easily identify which axioms are needed for a particular complex number proof, without the obfuscation of the set theory used to derive them. For more, see http://us.metamath.org/mpeuni/mmcomplex.html. When we wish to use a previously-proven assertion as an axiom, our convention is that we use the regular "ax-NAME" label naming convention to define the axiom, but we precede it with a proof of the same statement with the label "axNAME" . An example is complex arithmetic axiom ax-1cn 8797, proven by the preceding theorem ax1cn 8773. The metamath.exe program will warn if an axiom does not match the preceding theorem that justifies it if the names match in this way.
  • Definitions (df-...). We encourage definitions to include hypertext links to proven examples.
  • Statements with hypotheses. Many theorems and some axioms, such as ax-mp 8, have hypotheses that must be satisfied in order for the conclusion to hold, in this case min and maj. When presented in summarized form such as in the Theorem List (click on "Nearby theorems" on the ax-mp 8 page), the hypotheses are connected with an ampersand and separated from the conclusion with a big arrow, such as in "  |-  ph &  |-  ( ph  ->  ps ) =>  |-  ps". These symbols are not part of the Metamath language but are just informal notation meaning "and" and "implies".
  • Discouraged use and modification. If something should only be used in limited ways, it is marked with "(New usage is discouraged.)". This is used, for example, when something can be constructed in more than one way, and we do not want later theorems to depend on that specific construction. This marking is also used if we want later proofs to use proven axioms. For example, we want later proofs to use ax-1cn 8797 (not ax1cn 8773) and ax-1ne0 8808 (not ax1ne0 8784), as these are proven axioms for complex arithmetic. Thus, both ax1cn 8773 and ax1ne0 8784 are marked as "(New usage is discouraged.)". In some cases a proof should not normally be changed, e.g., when it demonstrates some specific technique. These are marked with "(Proof modification is discouraged.)".
  • New definitions infrequent. Typically, we are minimalist when introducing new definitions; they are introduced only when a clear advantage becomes apparent for reducing the number of symbols, shortening proofs, etc. We generally avoid the introduction of gratuitous definitions because each one requires associated theorems and additional elimination steps in proofs. For example, we use  < and  <_ for inequality expressions, and use  ( ( sin `  ( _i  x.  A ) )  /  _i ) instead of  (sinh `  A ) for the hyperbolic sine.
  • Axiom of choice. The axiom of choice (df-ac 7745) is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics. However, there have been and still are some lingering controversies about the Axiom of Choice. Therefore, where a proof does not require the axiom of choice, we prefer that proof instead. E.g., our proof of the Schroeder-Bernstein Theorem (sbth 6983) does not use the axiom of choice. In some cases, the weaker axiom of countable choice (ax-cc 8063) or axiom of dependent choice (ax-dc 8074) can be used instead.
  • Variables. Typically, Greek letters ( ph = phi,  ps = psi,  ch = chi, etc.),... are used for propositional (wff) variables;  x,  y,  z,... for individual (set) variables; and  A,  B,  C,... for class variables.
  • Turnstile. " |-", meaning "It is provable that," is the first token of all assertions and hypotheses that aren't syntax constructions. This is a standard convention in logic. For us, it also prevents any ambiguity with statements that are syntax constructions, such as "wff  -.  ph".
  • Biconditional ( <->). There are basically two ways to maximize the effectiveness of biconditionals ( <->): you can either have one-directional simplifications of all theorems that produce biconditionals, or you can have one-directional simplifications of theorems that consume biconditionals. Some tools (like Lean) follow the first approach, but set.mm follows the second approach. Practically, this means that in set.mm, for every theorem that uses an implication in the hypothesis, like ax-mp 8, there is a corresponding version with a biconditional or a reversed biconditional, like mpbi 199 or mpbir 200. We prefer this second approach because the number of duplications in the second approach is bounded by the size of the propositional calculus section, which is much smaller than the number of possible theorems in all later sections that produce biconditionals. So although theorems like biimpi 186 are available, in most cases there is already a theorem that combines it with your theorem of choice, like mpbir2an 886, sylbir 204, or 3imtr4i 257.
  • Substitution. " [ y  /  x ] ph" should be read "the wff that results from the proper substitution of  y for  x in wff  ph." See df-sb 1632 and the related df-sbc 2994 and df-csb 3084.
  • Is-a set. " A  e.  _V" should be read "Class  A is a set (i.e. exists)." This is a convenient convention based on Definition 2.9 of [Quine] p. 19. See df-v 2792 and isset 2794.
  • Converse. " `' R" should be read "converse of (relation)  R" and is the same as the more standard notation R^{-1} (the standard notation is ambiguous). See df-cnv 4699. This can be used to define a subset, e.g., df-tan 12355 notates "the set of values whose cosine is a nonzero complex number" as  ( `' cos " ( CC  \  { 0 } ) ).
  • Function application. "( F `  x)" should be read "the value of function  F at  x" and has the same meaning as the more familiar but ambiguous notation F(x). For example,  ( cos `  0 )  =  1 (see cos0 12432). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. See df-fv 5265. In the ASCII (input) representation there are spaces around the grave accent; there is a single accent when it is used directly, and it is doubled within comments.
  • Infix and parentheses. When a function that takes two classes and produces a class is applied as part of an infix expression, the expression is always surrounded by parentheses (see df-ov 5863). For example, the  + in  ( 2  +  2 ); see 2p2e4 9844. Function application is itself an example of this. Similarly, predicate expressions in infix form that take two or three wffs and produce a wff are also always surrounded by parentheses, such as  ( ph  ->  ps ),  ( ph  \/  ps ),  ( ph  /\  ps ), and  ( ph  <->  ps ) (see wi 4, df-or 359, df-an 360, and df-bi 177 respectively). In contrast, a binary relation (which compares two classes and produces a wff) applied in an infix expression is not surrounded by parentheses. This includes set membership  A  e.  B (see wel 1687), equality  A  =  B (see df-cleq 2278), subset  A  C_  B (see df-ss 3168), and less-than  A  <  B (see df-lt 8752). For the general definition of a binary relation in the form  A R B, see df-br 4026. For example,  0  <  1 ( see 0lt1 9298) does not use parentheses.
  • Unary minus. The symbol  -u is used to indicate a unary minus, e.g.,  -u 1. It is specially defined because it is so commonly used. See cneg 9040.
  • Function definition. Functions are typically defined by first defining the constant symbol (using $c) and declaring that its symbol is a class with the label cNAME (e.g., ccos 12348). The function is then defined labelled df-NAME; definitions are typically given using the maps-to notation (e.g., df-cos 12354). Typically, there are other proofs such as its closure labelled NAMEcl (e.g., coscl 12409), its function application form labelled NAMEval (e.g., cosval 12405), and at least one simple value (e.g., cos0 12432).
  • Factorial. The factorial function is traditionally a postfix operation, but we treat it as a normal function applied in prefix form, e.g.,  ( ! `  4 )  = ; 2 4 (df-fac 11291 and fac4 11298).
  • Unambiguous symbols. A given symbol has a single unambiguous meaning in general. Thus, where the literature might use the same symbol with different meanings, here we use different (variant) symbols for different meanings. These variant symbols often have suffixes, subscripts, or underlines to distinguish them. For example, here " 0" always means the value zero (df-0 8746), while " 0g" is the group identity element (df-0g 13406), " 0." is the poset zero (df-p0 14147), " 0 p" is the zero polynomial (df-0p 19027), " 0vec" is the zero vector in a normed complex vector space (df-0v 21156), and " .0." is a class variable for use as a connective symbol (this is used, for example, in p0val 14149). There are other class variables used as connective symbols where traditional notation would use ambiguous symbols, including " .1.", " .+", " .*", and " .||". These symbols are very similar to traditional notation, but because they are different symbols they eliminate ambiguity.
  • Natural numbers. There are different definitions of "natural" numbers in the literature. We use  NN (df-nn 9749) for the integer numbers starting from 1, and  NN0 (df-n0 9968) for the set of nonnegative integers starting at zero.
  • Decimal numbers. Numbers larger than ten are often expressed in base 10 using the decimal constructor df-dec 10127, e.g., ;;; 4 0 0 1 (see 4001prm 13145 for a proof that 4001 is prime).
  • Theorem forms. We often call a theorem a "deduction" whenever the conclusion and all hypotheses are each prefixed with the same antecedent  ph  ->. Deductions are often the preferred form for theorems because they allow us to easily use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used. See, for example, a1d 22. A deduction hypothesis can have an indirect antecedent via definitions, e.g., see lhop 19365. Deductions have a label suffix of "d" if there are other forms of the same theorem. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 10. Finally, a "tautology" would be the form with no hypotheses, and its label would have no suffix. For example, see pm2.43 47, pm2.43i 43, and pm2.43d 44.
  • Deduction theorem. The Deduction Theorem is a metalogical theorem that provides an algorithm for constructing a proof of a theorem from the proof of its corresponding deduction. In ordinary mathematics, no one actually carries out the algorithm, because (in its most basic form) it involves an exponential explosion of the number of proof steps as more hypotheses are eliminated. Instead, in ordinary mathematics the Deduction Theorem is invoked simply to claim that something can be done in principle, without actually doing it. For more details, see http://us.metamath.org/mpeuni/mmdeduction.html. The Deduction Theorem is a metalogical theorem that cannot be applied directly in metamath, and the explosion of steps would be a problem anyway, so alternatives are used. One alternative we use sometimes is the "weak deduction theorem" dedth 3608, which works in certain cases in set theory. We also sometimes use dedhb 2937. However, the primary mechanism we use today for emulating the deduction theorem is to write proofs in the deduction theorem form (aka "deduction style") described earlier; the prefixed  ph  -> mimics the context in a deduction proof system. In practice this mechanism works very well. This approach is described in the deduction form and natural deduction page; a list of translations for common natural deduction rules is given in natded 20792.
  • Recursion. We define recursive functions using various "recursion constructors". These allow us to define, with compact direct definitions, functions that are usually defined in textbooks with indirect self-referencing recursive definitions. This produces compact definition and much simpler proofs, and greatly reduces the risk of creating unsound definitions. Examples of recursion constructors include recs ( F ) in df-recs 6390,  rec ( F ,  I ) in df-rdg 6425, seq𝜔 ( F ,  I ) in df-seqom 6462, and  seq  M (  .+  ,  F ) in df-seq 11049. These have characteristic function  F and initial value  I. ( gsumg in df-gsum 13407 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6390, but for the "average user" the most useful one is probably df-seq 11049- provided that a countable sequence is sufficient for the recursion.
  • Extensible structures. Mathematics includes many structures such as ring, group, poset, etc. We define an "extensible structure" which is then used to define group, ring, poset, etc. This allows theorems from more general structures (groups) to be reused for more specialized structures (rings) without having to reprove them. See df-struct 13152.
  • Organizing proofs. Humans have trouble understanding long proofs. It is often preferable to break longer proofs into smaller parts (just as with traditional proofs). In Metamath this is done by creating separate proofs of the separate parts. A proof with the sole purpose of supporting a final proof is a lemma; the naming convention for a lemma is the final proof's name followed by "lem", and a number if there is more than one. E.g., sbthlem1 6973 is the first lemma for sbth 6983. Also, consider proving reusable results separately, so that others will be able to easily reuse that part of your work.
  • Hypertext links. We strongly encourage comments to have many links to related material, with accompanying text that explains the relationship. These can help readers understand the context. Links to other statements, or to HTTP/HTTPS URLs, can be inserted in ASCII source text by prepending a space-separated tilde. When metamath.exe is used to generate HTML it automatically inserts hypertext links for syntax used (e.g., every symbol used), every axiom and definition depended on, the justification for each step in a proof, and to both the next and previous assertion.
  • Bibliography references. Please include a bibliographic reference to any external material used. A name in square brackets in a comment indicates a bibliographic reference. The full reference must be of the form KEYWORD IDENTIFIER? NOISEWORD(S)* [AUTHOR(S)] p. NUMBER - note that this is a very specific form that requires a page number. There should be no comma between the author reference and the "p." (a constant indicator). Whitespace, comma, period, or semicolon should follow NUMBER. An example is Theorem 3.1 of [Monk1] p. 22, The KEYWORD, which is not case-sensitive, must be one of the following: Axiom, Chapter, Compare, Condition, Corollary, Definition, Equation, Example, Exercise, Figure, Item, Lemma, Lemmas, Line, Lines, Notation, Part, Postulate, Problem, Property, Proposition, Remark, Rule, Scheme, Section, or Theorem. The IDENTIFIER is optional, as in for example "Remark in [Monk1] p. 22". The NOISEWORDS(S) are zero or more from the list: from, in, of, on. The AUTHOR(S) must be present in the file identified with the htmlbibliography assignment (e.g. mmset.html) as a named anchor (NAME=). If there is more than one document by the same author(s), add a numeric suffix (as shown here). The NUMBER is a page number, and may be any alphanumeric string such as an integer or Roman numeral. Note that we require page numbers in comments for individual $a or $p statements. We allow names in square brackets without page numbers (a reference to an entire document) in heading comments. If this is a new reference, please also add it to the "Bibliography" section of mmset.html. (The file mmbiblio.html is automatically rebuilt, e.g., using the metamath.exe "write bibliography" command.)
  • Input format. The input is in ASCII with two-space indents. Tab characters are not allowed. Use embedded math comments or HTML entities for non-ASCII characters (e.g., "&eacute;" for "é").
  • Information on syntax, axioms, and definitions. For a hyperlinked list of syntax, axioms, and definitions, see http://us.metamath.org/mpeuni/mmdefinitions.html. If you have questions about a specific symbol or axiom, it is best to go directly to its definition to learn more about it. The generated HTML for each theorem and axiom includes hypertext links to each symbol's definition.

Naming conventions

Every statement has a unique identifying label. We use various label naming conventions to provide easy-to-remember hints about their contents. Labels are not a 1-to-1 mapping, because that would create long names that would be difficult to remember and tedious to type. Instead, label names are relatively short while suggesting their purpose. Names are occasionally changed to make them more consistent or as we find better ways to name them. Here are a few of the label naming conventions:

  • Axioms, definitions, and wff syntax. As noted earlier, axioms are named "ax-NAME", proofs of proven axioms are named "axNAME", and definitions are named "df-NAME". Wff syntax declarations have labels beginning with "w" followed by short fragment suggesting its purpose.
  • Hypotheses. Hypotheses have the name of the final axiom or theorem, followed by ".", followed by a unique id.
  • Common names. If a theorem has a well-known name, that name (or a short version of it) is sometimes used directly. Examples include barbara 2242 and stirling 27849.
  • Syntax label fragments. Most theorems are named using syntax label fragments. Almost every syntactic construct has a definition labelled "df-NAME", and NAME normally is the syntax label fragment. For example, the difference construct  ( A  \  B ) is defined in df-dif 3157, and thus its syntax label fragment is "dif". Similarly, the singleton construct  { A } has syntax label fragment "sn" (because it is defined in df-sn 3648), the subclass (subset) relation  A  C_  B has "ss" (because it is defined in df-ss 3168), and the pair construct  { A ,  B } has "pr" (df-pr 3649). Theorem names are often a concatenation of the syntax label fragments (omitting variables). For example, a theorem about  ( A  \  B )  C_  A involves a difference ("dif") of a subset ("ss"), and thus is named difss 3305. Digits are used to represent themselves. Suffixes (e.g., with numbers) are sometimes used to distinguish multiple theorems that would otherwise produce the same label.
  • Phantom definitions. In some cases there are common label fragments for something that could be in a definition, but for technical reasons is not. The is-element-of (is member of) construct  A  e.  B does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with  ( A  e.  ( B  \  { C } ) uses is-element-of ("el") of a difference ("dif") of a singleton ("sn"), it is named eldifsn 3751. An "n" is often used for negation ( -.), e.g., nan 563.
  • Exceptions. Sometimes there is a definition df-NAME but the label fragment is not the NAME part. The table below attempts to list all such cases and marks them in bold. For example, label fragment "cn" represents complex numbers  CC (even though its definition is in df-c 8745) and "re" represents real numbers  RR. The empty set  (/) often uses fragment 0, even though it is defined in df-nul 3458. Syntax construct  ( A  +  B ) usually uses the fragment "add" (which is consistent with df-add 8750), but "p" is used as the fragment for constant theorems. Equality  ( A  =  B ) often uses "e" as the fragment. As a result, "two plus two equals four" is named 2p2e4 9844.
  • Other markings. In labels we sometimes use "com" for "commutative", "ass" for "associative", "rot" for "rotation", and "di" for "distributive".
  • Principia Mathematica. Proofs of theorems from Principia Mathematica often use a different naming convention. They are instead often named "pm" followed by its identifier. For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named pm2.27 35.
  • Closures and values. As noted above, if a function df-NAME is defined, there is typically a proof of its value named "NAMEval" and its closure named "NAMEcl". E.g., for cosine (df-cos 12354) we have value cosval 12405 and closure coscl 12409.
  • Special cases. Sometimes syntax and related markings are insufficient to distinguish different theorems. For example, there are over 100 different implication-exclusive theorems. These are then grouped in a more ad-hoc way that attempts to make their distinctions clearer. These often use abbreviations such as "mp" for "modus ponens", "syl" for syllogism, and "id" for "identity". It's especially hard to give good names in the propositional calculus section because there are so few primitives. However, in most cases this is not a serious problem. There are a few very common theorems like ax-mp 8 and syl 15 that you will have no trouble remembering, a few theorem series like syl*anc and simp* that you can use parametrically, and a few other useful glue things for destructuring 'and's and 'or's (see natded 20792 for a list), and that's about all you need for most things. As for the rest, you can just assume that if it involves three or less connectives we probably already have a proof, and searching for it will give you the name.
  • Suffixes. We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as  F/ x ph in 19.21 1793 via the use of distinct variable conditions combined with nfv 1607. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2151 derived from df-eu 2149. The "f" stands for "not free in" which is less restrictive than "does not occur in." We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 15) -type inference in a pr