Metamath Proof Explorer

Theorem selberg3lem2

Description: Lemma for selberg3 . Equation 10.4.21 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion selberg3lem2 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) e. O(1)

Proof

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