Metamath Proof Explorer

Theorem selbergb

Description: Convert eventual boundedness in selberg to boundedness on [ 1 , +oo ) . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016)

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