Metamath Proof Explorer

Theorem logdivsum

Description: Asymptotic analysis of sum_ n <_ x , log n / n = ( log x ) ^ 2 / 2 + L + O ( log x / x ) . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypothesis logdivsum.1 
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
Assertion logdivsum 
|- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) )

Proof

Step Hyp Ref Expression
1 logdivsum.1 
 |-  F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
2 ioorp 
 |-  ( 0 (,) +oo ) = RR+
3 2 eqcomi 
 |-  RR+ = ( 0 (,) +oo )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( T. -> 1 e. ZZ )
6 ere 
 |-  _e e. RR
7 6 a1i 
 |-  ( T. -> _e e. RR )
8 0re 
 |-  0 e. RR
9 epos 
 |-  0 < _e
10 8 6 9 ltleii 
 |-  0 <_ _e
11 10 a1i 
 |-  ( T. -> 0 <_ _e )
12 1re 
 |-  1 e. RR
13 addge02 
 |-  ( ( 1 e. RR /\ _e e. RR ) -> ( 0 <_ _e <-> 1 <_ ( _e + 1 ) ) )
14 12 6 13 mp2an 
 |-  ( 0 <_ _e <-> 1 <_ ( _e + 1 ) )
15 11 14 sylib 
 |-  ( T. -> 1 <_ ( _e + 1 ) )
16 8 a1i 
 |-  ( T. -> 0 e. RR )
17 relogcl 
 |-  ( y e. RR+ -> ( log ` y ) e. RR )
18 17 adantl 
 |-  ( ( T. /\ y e. RR+ ) -> ( log ` y ) e. RR )
19 18 resqcld 
 |-  ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) ^ 2 ) e. RR )
20 19 rehalfcld 
 |-  ( ( T. /\ y e. RR+ ) -> ( ( ( log ` y ) ^ 2 ) / 2 ) e. RR )
21 rerpdivcl 
 |-  ( ( ( log ` y ) e. RR /\ y e. RR+ ) -> ( ( log ` y ) / y ) e. RR )
22 17 21 mpancom 
 |-  ( y e. RR+ -> ( ( log ` y ) / y ) e. RR )
23 22 adantl 
 |-  ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) / y ) e. RR )
24 nnrp 
 |-  ( y e. NN -> y e. RR+ )
25 24 23 sylan2 
 |-  ( ( T. /\ y e. NN ) -> ( ( log ` y ) / y ) e. RR )
26 reelprrecn 
 |-  RR e. { RR , CC }
27 26 a1i 
 |-  ( T. -> RR e. { RR , CC } )
28 cnelprrecn 
 |-  CC e. { RR , CC }
29 28 a1i 
 |-  ( T. -> CC e. { RR , CC } )
30 18 recnd 
 |-  ( ( T. /\ y e. RR+ ) -> ( log ` y ) e. CC )
31 ovexd 
 |-  ( ( T. /\ y e. RR+ ) -> ( 1 / y ) e. _V )
32 sqcl 
 |-  ( x e. CC -> ( x ^ 2 ) e. CC )
33 32 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( x ^ 2 ) e. CC )
34 33 halfcld 
 |-  ( ( T. /\ x e. CC ) -> ( ( x ^ 2 ) / 2 ) e. CC )
35 simpr 
 |-  ( ( T. /\ x e. CC ) -> x e. CC )
36 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
37 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
38 36 37 mp1i 
 |-  ( T. -> ( log |` RR+ ) : RR+ --> RR )
39 38 feqmptd 
 |-  ( T. -> ( log |` RR+ ) = ( y e. RR+ |-> ( ( log |` RR+ ) ` y ) ) )
40 fvres 
 |-  ( y e. RR+ -> ( ( log |` RR+ ) ` y ) = ( log ` y ) )
41 40 mpteq2ia 
 |-  ( y e. RR+ |-> ( ( log |` RR+ ) ` y ) ) = ( y e. RR+ |-> ( log ` y ) )
42 39 41 eqtrdi 
 |-  ( T. -> ( log |` RR+ ) = ( y e. RR+ |-> ( log ` y ) ) )
43 42 oveq2d 
 |-  ( T. -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( y e. RR+ |-> ( log ` y ) ) ) )
44 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( y e. RR+ |-> ( 1 / y ) )
45 43 44 eqtr3di 
 |-  ( T. -> ( RR _D ( y e. RR+ |-> ( log ` y ) ) ) = ( y e. RR+ |-> ( 1 / y ) ) )
46 ovexd 
 |-  ( ( T. /\ x e. CC ) -> ( 2 x. x ) e. _V )
47 2nn 
 |-  2 e. NN
48 dvexp 
 |-  ( 2 e. NN -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) )
49 47 48 mp1i 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) )
50 2m1e1 
 |-  ( 2 - 1 ) = 1
51 50 oveq2i 
 |-  ( x ^ ( 2 - 1 ) ) = ( x ^ 1 )
52 exp1 
 |-  ( x e. CC -> ( x ^ 1 ) = x )
53 52 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( x ^ 1 ) = x )
54 51 53 eqtrid 
 |-  ( ( T. /\ x e. CC ) -> ( x ^ ( 2 - 1 ) ) = x )
55 54 oveq2d 
 |-  ( ( T. /\ x e. CC ) -> ( 2 x. ( x ^ ( 2 - 1 ) ) ) = ( 2 x. x ) )
56 55 mpteq2dva 
 |-  ( T. -> ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) = ( x e. CC |-> ( 2 x. x ) ) )
57 49 56 eqtrd 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. x ) ) )
58 2cnd 
 |-  ( T. -> 2 e. CC )
59 2ne0 
 |-  2 =/= 0
60 59 a1i 
 |-  ( T. -> 2 =/= 0 )
61 29 33 46 57 58 60 dvmptdivc 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( ( x ^ 2 ) / 2 ) ) ) = ( x e. CC |-> ( ( 2 x. x ) / 2 ) ) )
62 2cn 
 |-  2 e. CC
63 divcan3 
 |-  ( ( x e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. x ) / 2 ) = x )
64 62 59 63 mp3an23 
 |-  ( x e. CC -> ( ( 2 x. x ) / 2 ) = x )
65 64 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( ( 2 x. x ) / 2 ) = x )
66 65 mpteq2dva 
 |-  ( T. -> ( x e. CC |-> ( ( 2 x. x ) / 2 ) ) = ( x e. CC |-> x ) )
67 61 66 eqtrd 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( ( x ^ 2 ) / 2 ) ) ) = ( x e. CC |-> x ) )
68 oveq1 
 |-  ( x = ( log ` y ) -> ( x ^ 2 ) = ( ( log ` y ) ^ 2 ) )
69 68 oveq1d 
 |-  ( x = ( log ` y ) -> ( ( x ^ 2 ) / 2 ) = ( ( ( log ` y ) ^ 2 ) / 2 ) )
70 id 
 |-  ( x = ( log ` y ) -> x = ( log ` y ) )
71 27 29 30 31 34 35 45 67 69 70 dvmptco 
 |-  ( T. -> ( RR _D ( y e. RR+ |-> ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) x. ( 1 / y ) ) ) )
72 rpcn 
 |-  ( y e. RR+ -> y e. CC )
73 72 adantl 
 |-  ( ( T. /\ y e. RR+ ) -> y e. CC )
74 rpne0 
 |-  ( y e. RR+ -> y =/= 0 )
75 74 adantl 
 |-  ( ( T. /\ y e. RR+ ) -> y =/= 0 )
76 30 73 75 divrecd 
 |-  ( ( T. /\ y e. RR+ ) -> ( ( log ` y ) / y ) = ( ( log ` y ) x. ( 1 / y ) ) )
77 76 mpteq2dva 
 |-  ( T. -> ( y e. RR+ |-> ( ( log ` y ) / y ) ) = ( y e. RR+ |-> ( ( log ` y ) x. ( 1 / y ) ) ) )
78 71 77 eqtr4d 
 |-  ( T. -> ( RR _D ( y e. RR+ |-> ( ( ( log ` y ) ^ 2 ) / 2 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) / y ) ) )
79 fveq2 
 |-  ( y = i -> ( log ` y ) = ( log ` i ) )
80 id 
 |-  ( y = i -> y = i )
81 79 80 oveq12d 
 |-  ( y = i -> ( ( log ` y ) / y ) = ( ( log ` i ) / i ) )
82 simp3r 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y <_ i )
83 simp2l 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y e. RR+ )
84 83 rpred 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> y e. RR )
85 simp3l 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e <_ y )
86 simp2r 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> i e. RR+ )
87 86 rpred 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> i e. RR )
88 6 a1i 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e e. RR )
89 88 84 87 85 82 letrd 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> _e <_ i )
90 logdivle 
 |-  ( ( ( y e. RR /\ _e <_ y ) /\ ( i e. RR /\ _e <_ i ) ) -> ( y <_ i <-> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) ) )
91 84 85 87 89 90 syl22anc 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> ( y <_ i <-> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) ) )
92 82 91 mpbid 
 |-  ( ( T. /\ ( y e. RR+ /\ i e. RR+ ) /\ ( _e <_ y /\ y <_ i ) ) -> ( ( log ` i ) / i ) <_ ( ( log ` y ) / y ) )
93 72 cxp1d 
 |-  ( y e. RR+ -> ( y ^c 1 ) = y )
94 93 oveq2d 
 |-  ( y e. RR+ -> ( ( log ` y ) / ( y ^c 1 ) ) = ( ( log ` y ) / y ) )
95 94 mpteq2ia 
 |-  ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) = ( y e. RR+ |-> ( ( log ` y ) / y ) )
96 1rp 
 |-  1 e. RR+
97 cxploglim 
 |-  ( 1 e. RR+ -> ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) ~~>r 0 )
98 96 97 mp1i 
 |-  ( T. -> ( y e. RR+ |-> ( ( log ` y ) / ( y ^c 1 ) ) ) ~~>r 0 )
99 95 98 eqbrtrrid 
 |-  ( T. -> ( y e. RR+ |-> ( ( log ` y ) / y ) ) ~~>r 0 )
100 fveq2 
 |-  ( y = A -> ( log ` y ) = ( log ` A ) )
101 id 
 |-  ( y = A -> y = A )
102 100 101 oveq12d 
 |-  ( y = A -> ( ( log ` y ) / y ) = ( ( log ` A ) / A ) )
103 3 4 5 7 15 16 20 23 25 78 81 92 1 99 102 dvfsumrlim3 
 |-  ( T. -> ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) ) )
104 103 mptru 
 |-  ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) )