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)