Metamath Proof Explorer

Theorem selberg2lem

Description: Lemma for selberg2 . Equation 10.4.12 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion selberg2lem 
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( x e. RR+ -> x e. RR )
2 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
3 1 2 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
4 3 recnd 
 |-  ( x e. RR+ -> ( psi ` x ) e. CC )
5 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
6 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
7 5 6 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) e. NN0 )
8 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
9 7 8 syl 
 |-  ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. NN )
10 9 nnrpd 
 |-  ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. RR+ )
11 10 relogcld 
 |-  ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) e. RR )
12 11 recnd 
 |-  ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) e. CC )
13 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
14 13 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
15 12 14 subcld 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC )
16 4 15 mulcld 
 |-  ( x e. RR+ -> ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. CC )
17 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
18 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
19 18 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
20 19 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
21 1rp 
 |-  1 e. RR+
22 rpaddcl 
 |-  ( ( n e. RR+ /\ 1 e. RR+ ) -> ( n + 1 ) e. RR+ )
23 21 22 mpan2 
 |-  ( n e. RR+ -> ( n + 1 ) e. RR+ )
24 23 relogcld 
 |-  ( n e. RR+ -> ( log ` ( n + 1 ) ) e. RR )
25 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
26 24 25 resubcld 
 |-  ( n e. RR+ -> ( ( log ` ( n + 1 ) ) - ( log ` n ) ) e. RR )
27 rpre 
 |-  ( n e. RR+ -> n e. RR )
28 chpcl 
 |-  ( n e. RR -> ( psi ` n ) e. RR )
29 27 28 syl 
 |-  ( n e. RR+ -> ( psi ` n ) e. RR )
30 26 29 remulcld 
 |-  ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. RR )
31 30 recnd 
 |-  ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC )
32 20 31 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC )
33 17 32 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC )
34 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
35 divsubdir 
 |-  ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. CC /\ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) )
36 16 33 34 35 syl3anc 
 |-  ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) )
37 4 12 mulcld 
 |-  ( x e. RR+ -> ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) e. CC )
38 4 14 mulcld 
 |-  ( x e. RR+ -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
39 37 38 33 sub32d 
 |-  ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) )
40 4 12 14 subdid 
 |-  ( x e. RR+ -> ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) )
41 40 oveq1d 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) )
42 fveq2 
 |-  ( m = n -> ( log ` m ) = ( log ` n ) )
43 fvoveq1 
 |-  ( m = n -> ( psi ` ( m - 1 ) ) = ( psi ` ( n - 1 ) ) )
44 42 43 jca 
 |-  ( m = n -> ( ( log ` m ) = ( log ` n ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( n - 1 ) ) ) )
45 fveq2 
 |-  ( m = ( n + 1 ) -> ( log ` m ) = ( log ` ( n + 1 ) ) )
46 fvoveq1 
 |-  ( m = ( n + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) )
47 45 46 jca 
 |-  ( m = ( n + 1 ) -> ( ( log ` m ) = ( log ` ( n + 1 ) ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) ) )
48 fveq2 
 |-  ( m = 1 -> ( log ` m ) = ( log ` 1 ) )
49 log1 
 |-  ( log ` 1 ) = 0
50 48 49 eqtrdi 
 |-  ( m = 1 -> ( log ` m ) = 0 )
51 oveq1 
 |-  ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
52 1m1e0 
 |-  ( 1 - 1 ) = 0
53 51 52 eqtrdi 
 |-  ( m = 1 -> ( m - 1 ) = 0 )
54 53 fveq2d 
 |-  ( m = 1 -> ( psi ` ( m - 1 ) ) = ( psi ` 0 ) )
55 2pos 
 |-  0 < 2
56 0re 
 |-  0 e. RR
57 chpeq0 
 |-  ( 0 e. RR -> ( ( psi ` 0 ) = 0 <-> 0 < 2 ) )
58 56 57 ax-mp 
 |-  ( ( psi ` 0 ) = 0 <-> 0 < 2 )
59 55 58 mpbir 
 |-  ( psi ` 0 ) = 0
60 54 59 eqtrdi 
 |-  ( m = 1 -> ( psi ` ( m - 1 ) ) = 0 )
61 50 60 jca 
 |-  ( m = 1 -> ( ( log ` m ) = 0 /\ ( psi ` ( m - 1 ) ) = 0 ) )
62 fveq2 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( log ` m ) = ( log ` ( ( |_ ` x ) + 1 ) ) )
63 fvoveq1 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
64 62 63 jca 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( log ` m ) = ( log ` ( ( |_ ` x ) + 1 ) ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
65 nnuz 
 |-  NN = ( ZZ>= ` 1 )
66 9 65 eleqtrdi 
 |-  ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
67 elfznn 
 |-  ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
68 67 adantl 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
69 68 nnrpd 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ )
70 69 relogcld 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( log ` m ) e. RR )
71 70 recnd 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( log ` m ) e. CC )
72 68 nnred 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
73 peano2rem 
 |-  ( m e. RR -> ( m - 1 ) e. RR )
74 72 73 syl 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
75 chpcl 
 |-  ( ( m - 1 ) e. RR -> ( psi ` ( m - 1 ) ) e. RR )
76 74 75 syl 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( m - 1 ) ) e. RR )
77 76 recnd 
 |-  ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( m - 1 ) ) e. CC )
78 44 47 61 64 66 71 77 fsumparts 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) ) )
79 7 nn0zd 
 |-  ( x e. RR+ -> ( |_ ` x ) e. ZZ )
80 fzval3 
 |-  ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
81 79 80 syl 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
82 81 eqcomd 
 |-  ( x e. RR+ -> ( 1 ..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
83 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
84 19 83 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. NN0 )
85 84 nn0red 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
86 chpcl 
 |-  ( ( n - 1 ) e. RR -> ( psi ` ( n - 1 ) ) e. RR )
87 85 86 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. RR )
88 87 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. CC )
89 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
90 19 89 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
91 90 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
92 19 nncnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
93 ax-1cn 
 |-  1 e. CC
94 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
95 92 93 94 sylancl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
96 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
97 92 93 96 sylancl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n - 1 ) + 1 ) = n )
98 95 97 eqtr4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = ( ( n - 1 ) + 1 ) )
99 98 fveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( psi ` ( ( n - 1 ) + 1 ) ) )
100 chpp1 
 |-  ( ( n - 1 ) e. NN0 -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) )
101 84 100 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) )
102 97 fveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` ( ( n - 1 ) + 1 ) ) = ( Lam ` n ) )
103 102 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) )
104 99 101 103 3eqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) )
105 88 91 104 mvrladdd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) = ( Lam ` n ) )
106 105 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( log ` n ) x. ( Lam ` n ) ) )
107 20 relogcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
108 107 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
109 91 108 mulcomd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) = ( ( log ` n ) x. ( Lam ` n ) ) )
110 106 109 eqtr4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( Lam ` n ) x. ( log ` n ) ) )
111 82 110 sumeq12rdv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) )
112 7 nn0cnd 
 |-  ( x e. RR+ -> ( |_ ` x ) e. CC )
113 pncan 
 |-  ( ( ( |_ ` x ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
114 112 93 113 sylancl 
 |-  ( x e. RR+ -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
115 114 fveq2d 
 |-  ( x e. RR+ -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` ( |_ ` x ) ) )
116 chpfl 
 |-  ( x e. RR -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) )
117 1 116 syl 
 |-  ( x e. RR+ -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) )
118 115 117 eqtrd 
 |-  ( x e. RR+ -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` x ) )
119 118 oveq2d 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` x ) ) )
120 12 4 mulcomd 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` x ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) )
121 119 120 eqtrd 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) )
122 0cn 
 |-  0 e. CC
123 122 mul01i 
 |-  ( 0 x. 0 ) = 0
124 123 a1i 
 |-  ( x e. RR+ -> ( 0 x. 0 ) = 0 )
125 121 124 oveq12d 
 |-  ( x e. RR+ -> ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - 0 ) )
126 37 subid1d 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - 0 ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) )
127 125 126 eqtrd 
 |-  ( x e. RR+ -> ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) )
128 95 fveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( psi ` n ) )
129 128 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) = ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) )
130 82 129 sumeq12rdv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) )
131 127 130 oveq12d 
 |-  ( x e. RR+ -> ( ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) )
132 78 111 131 3eqtr3d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) )
133 132 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) )
134 39 41 133 3eqtr4d 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) )
135 134 oveq1d 
 |-  ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) )
136 div23 
 |-  ( ( ( psi ` x ) e. CC /\ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) = ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) )
137 4 15 34 136 syl3anc 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) = ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) )
138 137 oveq1d 
 |-  ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) = ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) )
139 36 135 138 3eqtr3rd 
 |-  ( x e. RR+ -> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) )
140 139 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) )
141 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. _V )
142 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) e. _V )
143 reex 
 |-  RR e. _V
144 rpssre 
 |-  RR+ C_ RR
145 143 144 ssexi 
 |-  RR+ e. _V
146 145 a1i 
 |-  ( T. -> RR+ e. _V )
147 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. _V )
148 15 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC )
149 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) = ( x e. RR+ |-> ( ( psi ` x ) / x ) ) )
150 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) )
151 146 147 148 149 150 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) )
152 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
153 0red 
 |-  ( T. -> 0 e. RR )
154 1red 
 |-  ( T. -> 1 e. RR )
155 divrcnv 
 |-  ( 1 e. CC -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
156 93 155 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
157 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
158 157 rpred 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR )
159 158 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR )
160 11 13 resubcld 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. RR )
161 160 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. RR )
162 rpaddcl 
 |-  ( ( x e. RR+ /\ 1 e. RR+ ) -> ( x + 1 ) e. RR+ )
163 21 162 mpan2 
 |-  ( x e. RR+ -> ( x + 1 ) e. RR+ )
164 163 relogcld 
 |-  ( x e. RR+ -> ( log ` ( x + 1 ) ) e. RR )
165 164 13 resubcld 
 |-  ( x e. RR+ -> ( ( log ` ( x + 1 ) ) - ( log ` x ) ) e. RR )
166 7 nn0red 
 |-  ( x e. RR+ -> ( |_ ` x ) e. RR )
167 1red 
 |-  ( x e. RR+ -> 1 e. RR )
168 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
169 1 168 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) <_ x )
170 166 1 167 169 leadd1dd 
 |-  ( x e. RR+ -> ( ( |_ ` x ) + 1 ) <_ ( x + 1 ) )
171 10 163 logled 
 |-  ( x e. RR+ -> ( ( ( |_ ` x ) + 1 ) <_ ( x + 1 ) <-> ( log ` ( ( |_ ` x ) + 1 ) ) <_ ( log ` ( x + 1 ) ) ) )
172 170 171 mpbid 
 |-  ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) <_ ( log ` ( x + 1 ) ) )
173 11 164 13 172 lesub1dd 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( ( log ` ( x + 1 ) ) - ( log ` x ) ) )
174 logdifbnd 
 |-  ( x e. RR+ -> ( ( log ` ( x + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) )
175 160 165 158 173 174 letrd 
 |-  ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) )
176 175 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) )
177 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
178 1 177 syl 
 |-  ( x e. RR+ -> x <_ ( ( |_ ` x ) + 1 ) )
179 logleb 
 |-  ( ( x e. RR+ /\ ( ( |_ ` x ) + 1 ) e. RR+ ) -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) )
180 10 179 mpdan 
 |-  ( x e. RR+ -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) )
181 178 180 mpbid 
 |-  ( x e. RR+ -> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) )
182 11 13 subge0d 
 |-  ( x e. RR+ -> ( 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) )
183 181 182 mpbird 
 |-  ( x e. RR+ -> 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) )
184 183 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) )
185 153 154 156 159 161 176 184 rlimsqz2 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ~~>r 0 )
186 rlimo1 
 |-  ( ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ~~>r 0 -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) )
187 185 186 syl 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) )
188 o1mul 
 |-  ( ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) /\ ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) )
189 152 187 188 sylancr 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) )
190 151 189 eqeltrrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) )
191 nnrp 
 |-  ( m e. NN -> m e. RR+ )
192 191 ssriv 
 |-  NN C_ RR+
193 192 a1i 
 |-  ( T. -> NN C_ RR+ )
194 193 sselda 
 |-  ( ( T. /\ n e. NN ) -> n e. RR+ )
195 194 31 syl 
 |-  ( ( T. /\ n e. NN ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC )
196 chpo1ub 
 |-  ( n e. RR+ |-> ( ( psi ` n ) / n ) ) e. O(1)
197 196 a1i 
 |-  ( T. -> ( n e. RR+ |-> ( ( psi ` n ) / n ) ) e. O(1) )
198 rerpdivcl 
 |-  ( ( ( psi ` n ) e. RR /\ n e. RR+ ) -> ( ( psi ` n ) / n ) e. RR )
199 29 198 mpancom 
 |-  ( n e. RR+ -> ( ( psi ` n ) / n ) e. RR )
200 199 adantl 
 |-  ( ( T. /\ n e. RR+ ) -> ( ( psi ` n ) / n ) e. RR )
201 31 adantl 
 |-  ( ( T. /\ n e. RR+ ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC )
202 rpreccl 
 |-  ( n e. RR+ -> ( 1 / n ) e. RR+ )
203 202 rpred 
 |-  ( n e. RR+ -> ( 1 / n ) e. RR )
204 chpge0 
 |-  ( n e. RR -> 0 <_ ( psi ` n ) )
205 27 204 syl 
 |-  ( n e. RR+ -> 0 <_ ( psi ` n ) )
206 logdifbnd 
 |-  ( n e. RR+ -> ( ( log ` ( n + 1 ) ) - ( log ` n ) ) <_ ( 1 / n ) )
207 26 203 29 205 206 lemul1ad 
 |-  ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) <_ ( ( 1 / n ) x. ( psi ` n ) ) )
208 27 lep1d 
 |-  ( n e. RR+ -> n <_ ( n + 1 ) )
209 logleb 
 |-  ( ( n e. RR+ /\ ( n + 1 ) e. RR+ ) -> ( n <_ ( n + 1 ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) )
210 23 209 mpdan 
 |-  ( n e. RR+ -> ( n <_ ( n + 1 ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) )
211 208 210 mpbid 
 |-  ( n e. RR+ -> ( log ` n ) <_ ( log ` ( n + 1 ) ) )
212 24 25 subge0d 
 |-  ( n e. RR+ -> ( 0 <_ ( ( log ` ( n + 1 ) ) - ( log ` n ) ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) )
213 211 212 mpbird 
 |-  ( n e. RR+ -> 0 <_ ( ( log ` ( n + 1 ) ) - ( log ` n ) ) )
214 26 29 213 205 mulge0d 
 |-  ( n e. RR+ -> 0 <_ ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) )
215 30 214 absidd 
 |-  ( n e. RR+ -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) )
216 rpregt0 
 |-  ( n e. RR+ -> ( n e. RR /\ 0 < n ) )
217 divge0 
 |-  ( ( ( ( psi ` n ) e. RR /\ 0 <_ ( psi ` n ) ) /\ ( n e. RR /\ 0 < n ) ) -> 0 <_ ( ( psi ` n ) / n ) )
218 29 205 216 217 syl21anc 
 |-  ( n e. RR+ -> 0 <_ ( ( psi ` n ) / n ) )
219 199 218 absidd 
 |-  ( n e. RR+ -> ( abs ` ( ( psi ` n ) / n ) ) = ( ( psi ` n ) / n ) )
220 29 recnd 
 |-  ( n e. RR+ -> ( psi ` n ) e. CC )
221 rpcn 
 |-  ( n e. RR+ -> n e. CC )
222 rpne0 
 |-  ( n e. RR+ -> n =/= 0 )
223 220 221 222 divrec2d 
 |-  ( n e. RR+ -> ( ( psi ` n ) / n ) = ( ( 1 / n ) x. ( psi ` n ) ) )
224 219 223 eqtrd 
 |-  ( n e. RR+ -> ( abs ` ( ( psi ` n ) / n ) ) = ( ( 1 / n ) x. ( psi ` n ) ) )
225 207 215 224 3brtr4d 
 |-  ( n e. RR+ -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) <_ ( abs ` ( ( psi ` n ) / n ) ) )
226 225 ad2antrl 
 |-  ( ( T. /\ ( n e. RR+ /\ 1 <_ n ) ) -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) <_ ( abs ` ( ( psi ` n ) / n ) ) )
227 154 197 200 201 226 o1le 
 |-  ( T. -> ( n e. RR+ |-> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) e. O(1) )
228 193 227 o1res2 
 |-  ( T. -> ( n e. NN |-> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) e. O(1) )
229 195 228 o1fsum 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) e. O(1) )
230 141 142 190 229 o1sub2 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) e. O(1) )
231 140 230 eqeltrrid 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1) )
232 231 mptru 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1)