Metamath Proof Explorer

Theorem chpdifbnd

Description: A bound on the difference of nearby psi values. Theorem 10.5.2 of Shapiro, p. 427. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Assertion chpdifbnd 
|- ( ( A e. RR /\ 1 <_ A ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selberg2b 
 |-  E. b e. RR+ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b
2 simpl 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A e. RR )
3 0red 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 e. RR )
4 1red 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 1 e. RR )
5 0lt1 
 |-  0 < 1
6 5 a1i 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 < 1 )
7 simpr 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 1 <_ A )
8 3 4 2 6 7 ltletrd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> 0 < A )
9 2 8 elrpd 
 |-  ( ( A e. RR /\ 1 <_ A ) -> A e. RR+ )
10 9 adantr 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( b e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b ) ) -> A e. RR+ )
11 simplr 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( b e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b ) ) -> 1 <_ A )
12 simprl 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( b e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b ) ) -> b e. RR+ )
13 simprr 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( b e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b ) ) -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b )
14 eqid 
 |-  ( ( b x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) = ( ( b x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )
15 10 11 12 13 14 chpdifbndlem2 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( b e. RR+ /\ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b ) ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) )
16 15 rexlimdvaa 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( E. b e. RR+ A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ n e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` n ) x. ( psi ` ( z / n ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ b -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) ) )
17 1 16 mpi 
 |-  ( ( A e. RR /\ 1 <_ A ) -> E. c e. RR+ A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( A x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) )