Metamath Proof Explorer

Theorem selberg2b

Description: Convert eventual boundedness in selberg2 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)

Ref Expression
Assertion selberg2b 
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
3 1 2 mp1i 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
4 3 simprbda 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR )
5 4 ex 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) -> x e. RR ) )
6 5 ssrdv 
 |-  ( T. -> ( 1 [,) +oo ) C_ RR )
7 1 a1i 
 |-  ( T. -> 1 e. RR )
8 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
9 4 8 syl 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( psi ` x ) e. RR )
10 1rp 
 |-  1 e. RR+
11 10 a1i 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR+ )
12 3 simplbda 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
13 4 11 12 rpgecld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> x e. RR+ )
14 13 relogcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( log ` x ) e. RR )
15 9 14 remulcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. RR )
16 fzfid 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
17 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
18 17 adantl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
19 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
20 18 19 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
21 4 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
22 21 18 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
23 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
24 22 23 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
25 20 24 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
26 16 25 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
27 15 26 readdcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) e. RR )
28 27 13 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) e. RR )
29 2re 
 |-  2 e. RR
30 29 a1i 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 2 e. RR )
31 30 14 remulcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. RR )
32 28 31 resubcld 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
33 32 recnd 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. CC )
34 13 ex 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) -> x e. RR+ ) )
35 34 ssrdv 
 |-  ( T. -> ( 1 [,) +oo ) C_ RR+ )
36 selberg2 
 |-  ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
37 36 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
38 35 37 o1res2 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
39 chpcl 
 |-  ( y e. RR -> ( psi ` y ) e. RR )
40 39 ad2antrl 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( psi ` y ) e. RR )
41 simprl 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR )
42 10 a1i 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 e. RR+ )
43 simprr 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 1 <_ y )
44 41 42 43 rpgecld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> y e. RR+ )
45 44 relogcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( log ` y ) e. RR )
46 40 45 remulcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( psi ` y ) x. ( log ` y ) ) e. RR )
47 fzfid 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin )
48 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` y ) ) -> n e. NN )
49 48 adantl 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN )
50 49 19 syl 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR )
51 41 adantr 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> y e. RR )
52 51 49 nndivred 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( y / n ) e. RR )
53 chpcl 
 |-  ( ( y / n ) e. RR -> ( psi ` ( y / n ) ) e. RR )
54 52 53 syl 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( psi ` ( y / n ) ) e. RR )
55 50 54 remulcld 
 |-  ( ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) e. RR )
56 47 55 fsumrecl 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) e. RR )
57 46 56 readdcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) e. RR )
58 29 a1i 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> 2 e. RR )
59 58 45 remulcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( 2 x. ( log ` y ) ) e. RR )
60 57 59 readdcld 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) + ( 2 x. ( log ` y ) ) ) e. RR )
61 32 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
62 61 recnd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. CC )
63 62 abscld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. RR )
64 28 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) e. RR )
65 64 recnd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) e. CC )
66 65 abscld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) e. RR )
67 31 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 2 x. ( log ` x ) ) e. RR )
68 67 recnd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 2 x. ( log ` x ) ) e. CC )
69 68 abscld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( 2 x. ( log ` x ) ) ) e. RR )
70 66 69 readdcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) + ( abs ` ( 2 x. ( log ` x ) ) ) ) e. RR )
71 60 ad2ant2r 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) + ( 2 x. ( log ` y ) ) ) e. RR )
72 65 68 abs2dif2d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ ( ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) + ( abs ` ( 2 x. ( log ` x ) ) ) ) )
73 simprll 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR )
74 73 39 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` y ) e. RR )
75 13 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR+ )
76 4 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x e. RR )
77 simprr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x < y )
78 76 73 77 ltled 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> x <_ y )
79 73 75 78 rpgecld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> y e. RR+ )
80 79 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` y ) e. RR )
81 74 80 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` y ) x. ( log ` y ) ) e. RR )
82 56 ad2ant2r 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) e. RR )
83 81 82 readdcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) e. RR )
84 29 a1i 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 2 e. RR )
85 84 80 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 2 x. ( log ` y ) ) e. RR )
86 76 8 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` x ) e. RR )
87 75 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) e. RR )
88 86 87 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. RR )
89 26 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
90 88 89 readdcld 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) e. RR )
91 chpge0 
 |-  ( x e. RR -> 0 <_ ( psi ` x ) )
92 76 91 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( psi ` x ) )
93 12 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 <_ x )
94 76 93 logge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( log ` x ) )
95 86 87 92 94 mulge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( psi ` x ) x. ( log ` x ) ) )
96 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
97 18 96 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
98 chpge0 
 |-  ( ( x / n ) e. RR -> 0 <_ ( psi ` ( x / n ) ) )
99 22 98 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( psi ` ( x / n ) ) )
100 20 24 97 99 mulge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
101 16 25 100 fsumge0 
 |-  ( ( T. /\ x e. ( 1 [,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
102 101 adantr 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
103 88 89 95 102 addge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
104 90 75 103 divge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) )
105 64 104 absidd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) )
106 10 a1i 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 1 e. RR+ )
107 chpwordi 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( psi ` x ) <_ ( psi ` y ) )
108 76 73 78 107 syl3anc 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( psi ` x ) <_ ( psi ` y ) )
109 75 79 logled 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( x <_ y <-> ( log ` x ) <_ ( log ` y ) ) )
110 78 109 mpbid 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( log ` x ) <_ ( log ` y ) )
111 86 74 87 80 92 94 108 110 lemul12ad 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( psi ` x ) x. ( log ` x ) ) <_ ( ( psi ` y ) x. ( log ` y ) ) )
112 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` y ) ) e. Fin )
113 48 adantl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. NN )
114 113 19 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( Lam ` n ) e. RR )
115 76 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> x e. RR )
116 115 113 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( x / n ) e. RR )
117 116 23 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( psi ` ( x / n ) ) e. RR )
118 114 117 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
119 112 118 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
120 113 96 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( Lam ` n ) )
121 116 98 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( psi ` ( x / n ) ) )
122 114 117 120 121 mulge0d 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
123 flword2 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) )
124 76 73 78 123 syl3anc 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) )
125 fzss2 
 |-  ( ( |_ ` y ) e. ( ZZ>= ` ( |_ ` x ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) )
126 124 125 syl 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` y ) ) )
127 112 118 122 126 fsumless 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
128 73 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> y e. RR )
129 128 113 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( y / n ) e. RR )
130 129 53 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( psi ` ( y / n ) ) e. RR )
131 114 130 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) e. RR )
132 113 nnrpd 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> n e. RR+ )
133 78 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> x <_ y )
134 115 128 132 133 lediv1dd 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( x / n ) <_ ( y / n ) )
135 chpwordi 
 |-  ( ( ( x / n ) e. RR /\ ( y / n ) e. RR /\ ( x / n ) <_ ( y / n ) ) -> ( psi ` ( x / n ) ) <_ ( psi ` ( y / n ) ) )
136 116 129 134 135 syl3anc 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( psi ` ( x / n ) ) <_ ( psi ` ( y / n ) ) )
137 117 130 114 120 136 lemul2ad 
 |-  ( ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) /\ n e. ( 1 ... ( |_ ` y ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) <_ ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) )
138 112 118 131 137 fsumle 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) )
139 89 119 82 127 138 letrd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) )
140 88 89 81 82 111 139 le2addd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) <_ ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) )
141 90 83 106 76 103 140 93 lediv12ad 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) <_ ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) / 1 ) )
142 83 recnd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) e. CC )
143 142 div1d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) / 1 ) = ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) )
144 141 143 breqtrd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) <_ ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) )
145 105 144 eqbrtrd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) <_ ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) )
146 2rp 
 |-  2 e. RR+
147 rpge0 
 |-  ( 2 e. RR+ -> 0 <_ 2 )
148 146 147 mp1i 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ 2 )
149 84 87 148 94 mulge0d 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> 0 <_ ( 2 x. ( log ` x ) ) )
150 67 149 absidd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( 2 x. ( log ` x ) ) ) = ( 2 x. ( log ` x ) ) )
151 87 80 84 148 110 lemul2ad 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( 2 x. ( log ` x ) ) <_ ( 2 x. ( log ` y ) ) )
152 150 151 eqbrtrd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( 2 x. ( log ` x ) ) ) <_ ( 2 x. ( log ` y ) ) )
153 66 69 83 85 145 152 le2addd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( ( abs ` ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) + ( abs ` ( 2 x. ( log ` x ) ) ) ) <_ ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) + ( 2 x. ( log ` y ) ) ) )
154 63 70 71 72 153 letrd 
 |-  ( ( ( T. /\ x e. ( 1 [,) +oo ) ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ ( ( ( ( psi ` y ) x. ( log ` y ) ) + sum_ n e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` n ) x. ( psi ` ( y / n ) ) ) ) + ( 2 x. ( log ` y ) ) ) )
155 6 7 33 38 60 154 o1bddrp 
 |-  ( T. -> E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c )
156 155 mptru 
 |-  E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c