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 + i = 1 y log i i log y 2 2
Assertion logdivsum F : + F dom F L A + e A F A L log A A

Proof

Step Hyp Ref Expression
1 logdivsum.1 F = y + i = 1 y log i i log y 2 2
2 ioorp 0 +∞ = +
3 2 eqcomi + = 0 +∞
4 nnuz = 1
5 1zzd 1
6 ere e
7 6 a1i e
8 0re 0
9 epos 0 < e
10 8 6 9 ltleii 0 e
11 10 a1i 0 e
12 1re 1
13 addge02 1 e 0 e 1 e + 1
14 12 6 13 mp2an 0 e 1 e + 1
15 11 14 sylib 1 e + 1
16 8 a1i 0
17 relogcl y + log y
18 17 adantl y + log y
19 18 resqcld y + log y 2
20 19 rehalfcld y + log y 2 2
21 rerpdivcl log y y + log y y
22 17 21 mpancom y + log y y
23 22 adantl y + log y y
24 nnrp y y +
25 24 23 sylan2 y log y y
26 reelprrecn
27 26 a1i
28 cnelprrecn
29 28 a1i
30 18 recnd y + log y
31 ovexd y + 1 y V
32 sqcl x x 2
33 32 adantl x x 2
34 33 halfcld x x 2 2
35 simpr x x
36 relogf1o log + : + 1-1 onto
37 f1of log + : + 1-1 onto log + : +
38 36 37 mp1i log + : +
39 38 feqmptd log + = y + log + y
40 fvres y + log + y = log y
41 40 mpteq2ia y + log + y = y + log y
42 39 41 eqtrdi log + = y + log y
43 42 oveq2d D log + = dy + log y d y
44 dvrelog D log + = y + 1 y
45 43 44 eqtr3di dy + log y d y = y + 1 y
46 ovexd x 2 x V
47 2nn 2
48 dvexp 2 dx x 2 d x = x 2 x 2 1
49 47 48 mp1i dx x 2 d x = x 2 x 2 1
50 2m1e1 2 1 = 1
51 50 oveq2i x 2 1 = x 1
52 exp1 x x 1 = x
53 52 adantl x x 1 = x
54 51 53 syl5eq x x 2 1 = x
55 54 oveq2d x 2 x 2 1 = 2 x
56 55 mpteq2dva x 2 x 2 1 = x 2 x
57 49 56 eqtrd dx x 2 d x = x 2 x
58 2cnd 2
59 2ne0 2 0
60 59 a1i 2 0
61 29 33 46 57 58 60 dvmptdivc dx x 2 2 d x = x 2 x 2
62 2cn 2
63 divcan3 x 2 2 0 2 x 2 = x
64 62 59 63 mp3an23 x 2 x 2 = x
65 64 adantl x 2 x 2 = x
66 65 mpteq2dva x 2 x 2 = x x
67 61 66 eqtrd dx x 2 2 d x = x 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 dy + log y 2 2 d y = y + log y 1 y
72 rpcn y + y
73 72 adantl y + y
74 rpne0 y + y 0
75 74 adantl y + y 0
76 30 73 75 divrecd y + log y y = log y 1 y
77 76 mpteq2dva y + log y y = y + log y 1 y
78 71 77 eqtr4d dy + log y 2 2 d y = y + 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 y + i + e y y i y i
83 simp2l y + i + e y y i y +
84 83 rpred y + i + e y y i y
85 simp3l y + i + e y y i e y
86 simp2r y + i + e y y i i +
87 86 rpred y + i + e y y i i
88 6 a1i y + i + e y y i e
89 88 84 87 85 82 letrd y + i + e y y i e i
90 logdivle y e y i e i y i log i i log y y
91 84 85 87 89 90 syl22anc y + i + e y y i y i log i i log y y
92 82 91 mpbid y + i + e y y i log i i log y y
93 72 cxp1d y + y 1 = y
94 93 oveq2d y + log y y 1 = log y y
95 94 mpteq2ia y + log y y 1 = y + log y y
96 1rp 1 +
97 cxploglim 1 + y + log y y 1 0
98 96 97 mp1i y + log y y 1 0
99 95 98 eqbrtrrid y + log y y 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 F : + F dom F L A + e A F A L log A A
104 103 mptru F : + F dom F L A + e A F A L log A A