Metamath Proof Explorer

Theorem chpdifbndlem2

Description: Lemma for chpdifbnd . (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypotheses chpdifbnd.a 
|- ( ph -> A e. RR+ )
chpdifbnd.1 
|- ( ph -> 1 <_ A )
chpdifbnd.b 
|- ( ph -> B e. RR+ )
chpdifbnd.2 
|- ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B )
chpdifbnd.c 
|- C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )
Assertion chpdifbndlem2 
|- ( ph -> 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 chpdifbnd.a 
 |-  ( ph -> A e. RR+ )
2 chpdifbnd.1 
 |-  ( ph -> 1 <_ A )
3 chpdifbnd.b 
 |-  ( ph -> B e. RR+ )
4 chpdifbnd.2 
 |-  ( ph -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B )
5 chpdifbnd.c 
 |-  C = ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) )
6 1rp 
 |-  1 e. RR+
7 rpaddcl 
 |-  ( ( A e. RR+ /\ 1 e. RR+ ) -> ( A + 1 ) e. RR+ )
8 1 6 7 sylancl 
 |-  ( ph -> ( A + 1 ) e. RR+ )
9 3 8 rpmulcld 
 |-  ( ph -> ( B x. ( A + 1 ) ) e. RR+ )
10 9 rpred 
 |-  ( ph -> ( B x. ( A + 1 ) ) e. RR )
11 2rp 
 |-  2 e. RR+
12 rpmulcl 
 |-  ( ( 2 e. RR+ /\ A e. RR+ ) -> ( 2 x. A ) e. RR+ )
13 11 1 12 sylancr 
 |-  ( ph -> ( 2 x. A ) e. RR+ )
14 13 rpred 
 |-  ( ph -> ( 2 x. A ) e. RR )
15 1 relogcld 
 |-  ( ph -> ( log ` A ) e. RR )
16 14 15 remulcld 
 |-  ( ph -> ( ( 2 x. A ) x. ( log ` A ) ) e. RR )
17 10 16 readdcld 
 |-  ( ph -> ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) e. RR )
18 9 rpgt0d 
 |-  ( ph -> 0 < ( B x. ( A + 1 ) ) )
19 13 rprege0d 
 |-  ( ph -> ( ( 2 x. A ) e. RR /\ 0 <_ ( 2 x. A ) ) )
20 log1 
 |-  ( log ` 1 ) = 0
21 logleb 
 |-  ( ( 1 e. RR+ /\ A e. RR+ ) -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) )
22 6 1 21 sylancr 
 |-  ( ph -> ( 1 <_ A <-> ( log ` 1 ) <_ ( log ` A ) ) )
23 2 22 mpbid 
 |-  ( ph -> ( log ` 1 ) <_ ( log ` A ) )
24 20 23 eqbrtrrid 
 |-  ( ph -> 0 <_ ( log ` A ) )
25 mulge0 
 |-  ( ( ( ( 2 x. A ) e. RR /\ 0 <_ ( 2 x. A ) ) /\ ( ( log ` A ) e. RR /\ 0 <_ ( log ` A ) ) ) -> 0 <_ ( ( 2 x. A ) x. ( log ` A ) ) )
26 19 15 24 25 syl12anc 
 |-  ( ph -> 0 <_ ( ( 2 x. A ) x. ( log ` A ) ) )
27 10 16 18 26 addgtge0d 
 |-  ( ph -> 0 < ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) )
28 17 27 elrpd 
 |-  ( ph -> ( ( B x. ( A + 1 ) ) + ( ( 2 x. A ) x. ( log ` A ) ) ) e. RR+ )
29 5 28 eqeltrid 
 |-  ( ph -> C e. RR+ )
30 1 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> A e. RR+ )
31 2 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> 1 <_ A )
32 3 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> B e. RR+ )
33 4 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> A. z e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` z ) x. ( log ` z ) ) + sum_ m e. ( 1 ... ( |_ ` z ) ) ( ( Lam ` m ) x. ( psi ` ( z / m ) ) ) ) / z ) - ( 2 x. ( log ` z ) ) ) ) <_ B )
34 simprl 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> x e. ( 1 (,) +oo ) )
35 simprr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> y e. ( x [,] ( A x. x ) ) )
36 30 31 32 33 5 34 35 chpdifbndlem1 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ y e. ( x [,] ( A x. x ) ) ) ) -> ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( C x. ( x / ( log ` x ) ) ) ) )
37 36 ralrimivva 
 |-  ( ph -> 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 ) ) ) ) )
38 oveq1 
 |-  ( c = C -> ( c x. ( x / ( log ` x ) ) ) = ( C x. ( x / ( log ` x ) ) ) )
39 38 oveq2d 
 |-  ( c = C -> ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) = ( ( 2 x. ( y - x ) ) + ( C x. ( x / ( log ` x ) ) ) ) )
40 39 breq2d 
 |-  ( c = C -> ( ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( c x. ( x / ( log ` x ) ) ) ) <-> ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( C x. ( x / ( log ` x ) ) ) ) ) )
41 40 2ralbidv 
 |-  ( c = C -> ( 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 ) ) ) ) <-> 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 ) ) ) ) ) )
42 41 rspcev 
 |-  ( ( 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 ) ) ) ) ) -> 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 ) ) ) ) )
43 29 37 42 syl2anc 
 |-  ( ph -> 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 ) ) ) ) )