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 syl5eq
 |-  ( ( 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 ) ) )