Metamath Proof Explorer


Theorem fsumharmonic

Description: Bound a finite sum based on the harmonic series, where the "strong" bound C only applies asymptotically, and there is a "weak" bound R for the remaining values. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses fsumharmonic.a φ A +
fsumharmonic.t φ T 1 T
fsumharmonic.r φ R 0 R
fsumharmonic.b φ n 1 A B
fsumharmonic.c φ n 1 A C
fsumharmonic.0 φ n 1 A 0 C
fsumharmonic.1 φ n 1 A T A n B C n
fsumharmonic.2 φ n 1 A A n < T B R
Assertion fsumharmonic φ n = 1 A B n n = 1 A C + R log T + 1

Proof

Step Hyp Ref Expression
1 fsumharmonic.a φ A +
2 fsumharmonic.t φ T 1 T
3 fsumharmonic.r φ R 0 R
4 fsumharmonic.b φ n 1 A B
5 fsumharmonic.c φ n 1 A C
6 fsumharmonic.0 φ n 1 A 0 C
7 fsumharmonic.1 φ n 1 A T A n B C n
8 fsumharmonic.2 φ n 1 A A n < T B R
9 fzfid φ 1 A Fin
10 elfznn n 1 A n
11 10 adantl φ n 1 A n
12 11 nncnd φ n 1 A n
13 11 nnne0d φ n 1 A n 0
14 4 12 13 divcld φ n 1 A B n
15 9 14 fsumcl φ n = 1 A B n
16 15 abscld φ n = 1 A B n
17 4 abscld φ n 1 A B
18 17 11 nndivred φ n 1 A B n
19 9 18 fsumrecl φ n = 1 A B n
20 9 5 fsumrecl φ n = 1 A C
21 3 simpld φ R
22 2 simpld φ T
23 0red φ 0
24 1red φ 1
25 0lt1 0 < 1
26 25 a1i φ 0 < 1
27 2 simprd φ 1 T
28 23 24 22 26 27 ltletrd φ 0 < T
29 22 28 elrpd φ T +
30 29 relogcld φ log T
31 30 24 readdcld φ log T + 1
32 21 31 remulcld φ R log T + 1
33 20 32 readdcld φ n = 1 A C + R log T + 1
34 9 14 fsumabs φ n = 1 A B n n = 1 A B n
35 4 12 13 absdivd φ n 1 A B n = B n
36 11 nnrpd φ n 1 A n +
37 36 rprege0d φ n 1 A n 0 n
38 absid n 0 n n = n
39 37 38 syl φ n 1 A n = n
40 39 oveq2d φ n 1 A B n = B n
41 35 40 eqtrd φ n 1 A B n = B n
42 41 sumeq2dv φ n = 1 A B n = n = 1 A B n
43 34 42 breqtrd φ n = 1 A B n n = 1 A B n
44 1 29 rpdivcld φ A T +
45 44 rprege0d φ A T 0 A T
46 flge0nn0 A T 0 A T A T 0
47 45 46 syl φ A T 0
48 47 nn0red φ A T
49 48 ltp1d φ A T < A T + 1
50 fzdisj A T < A T + 1 1 A T A T + 1 A =
51 49 50 syl φ 1 A T A T + 1 A =
52 nn0p1nn A T 0 A T + 1
53 47 52 syl φ A T + 1
54 nnuz = 1
55 53 54 eleqtrdi φ A T + 1 1
56 44 rpred φ A T
57 1 rpred φ A
58 22 28 jca φ T 0 < T
59 1 rpregt0d φ A 0 < A
60 lediv2 1 0 < 1 T 0 < T A 0 < A 1 T A T A 1
61 24 26 58 59 60 syl211anc φ 1 T A T A 1
62 27 61 mpbid φ A T A 1
63 57 recnd φ A
64 63 div1d φ A 1 = A
65 62 64 breqtrd φ A T A
66 flword2 A T A A T A A A T
67 56 57 65 66 syl3anc φ A A T
68 fzsplit2 A T + 1 1 A A T 1 A = 1 A T A T + 1 A
69 55 67 68 syl2anc φ 1 A = 1 A T A T + 1 A
70 18 recnd φ n 1 A B n
71 51 69 9 70 fsumsplit φ n = 1 A B n = n = 1 A T B n + n = A T + 1 A B n
72 fzfid φ 1 A T Fin
73 ssun1 1 A T 1 A T A T + 1 A
74 73 69 sseqtrrid φ 1 A T 1 A
75 74 sselda φ n 1 A T n 1 A
76 75 18 syldan φ n 1 A T B n
77 72 76 fsumrecl φ n = 1 A T B n
78 fzfid φ A T + 1 A Fin
79 ssun2 A T + 1 A 1 A T A T + 1 A
80 79 69 sseqtrrid φ A T + 1 A 1 A
81 80 sselda φ n A T + 1 A n 1 A
82 81 18 syldan φ n A T + 1 A B n
83 78 82 fsumrecl φ n = A T + 1 A B n
84 75 5 syldan φ n 1 A T C
85 72 84 fsumrecl φ n = 1 A T C
86 fznnfl A T n 1 A T n n A T
87 56 86 syl φ n 1 A T n n A T
88 87 simplbda φ n 1 A T n A T
89 36 rpred φ n 1 A n
90 57 adantr φ n 1 A A
91 58 adantr φ n 1 A T 0 < T
92 lemuldiv2 n A T 0 < T T n A n A T
93 89 90 91 92 syl3anc φ n 1 A T n A n A T
94 22 adantr φ n 1 A T
95 94 90 36 lemuldivd φ n 1 A T n A T A n
96 93 95 bitr3d φ n 1 A n A T T A n
97 75 96 syldan φ n 1 A T n A T T A n
98 88 97 mpbid φ n 1 A T T A n
99 7 ex φ n 1 A T A n B C n
100 75 99 syldan φ n 1 A T T A n B C n
101 98 100 mpd φ n 1 A T B C n
102 75 4 syldan φ n 1 A T B
103 102 abscld φ n 1 A T B
104 75 10 syl φ n 1 A T n
105 104 nnrpd φ n 1 A T n +
106 103 84 105 ledivmul2d φ n 1 A T B n C B C n
107 101 106 mpbird φ n 1 A T B n C
108 72 76 84 107 fsumle φ n = 1 A T B n n = 1 A T C
109 9 5 6 74 fsumless φ n = 1 A T C n = 1 A C
110 77 85 20 108 109 letrd φ n = 1 A T B n n = 1 A C
111 81 10 syl φ n A T + 1 A n
112 111 nnrecred φ n A T + 1 A 1 n
113 78 112 fsumrecl φ n = A T + 1 A 1 n
114 21 113 remulcld φ R n = A T + 1 A 1 n
115 21 adantr φ n A T + 1 A R
116 115 recnd φ n A T + 1 A R
117 111 nncnd φ n A T + 1 A n
118 111 nnne0d φ n A T + 1 A n 0
119 116 117 118 divrecd φ n A T + 1 A R n = R 1 n
120 115 111 nndivred φ n A T + 1 A R n
121 119 120 eqeltrrd φ n A T + 1 A R 1 n
122 81 17 syldan φ n A T + 1 A B
123 81 36 syldan φ n A T + 1 A n +
124 noel ¬ n
125 elin n 1 A T A T + 1 A n 1 A T n A T + 1 A
126 51 eleq2d φ n 1 A T A T + 1 A n
127 125 126 bitr3id φ n 1 A T n A T + 1 A n
128 124 127 mtbiri φ ¬ n 1 A T n A T + 1 A
129 imnan n 1 A T ¬ n A T + 1 A ¬ n 1 A T n A T + 1 A
130 128 129 sylibr φ n 1 A T ¬ n A T + 1 A
131 130 con2d φ n A T + 1 A ¬ n 1 A T
132 131 imp φ n A T + 1 A ¬ n 1 A T
133 86 baibd A T n n 1 A T n A T
134 56 10 133 syl2an φ n 1 A n 1 A T n A T
135 134 96 bitrd φ n 1 A n 1 A T T A n
136 81 135 syldan φ n A T + 1 A n 1 A T T A n
137 132 136 mtbid φ n A T + 1 A ¬ T A n
138 57 adantr φ n A T + 1 A A
139 138 111 nndivred φ n A T + 1 A A n
140 22 adantr φ n A T + 1 A T
141 139 140 ltnled φ n A T + 1 A A n < T ¬ T A n
142 137 141 mpbird φ n A T + 1 A A n < T
143 8 ex φ n 1 A A n < T B R
144 81 143 syldan φ n A T + 1 A A n < T B R
145 142 144 mpd φ n A T + 1 A B R
146 122 115 123 145 lediv1dd φ n A T + 1 A B n R n
147 146 119 breqtrd φ n A T + 1 A B n R 1 n
148 78 82 121 147 fsumle φ n = A T + 1 A B n n = A T + 1 A R 1 n
149 21 recnd φ R
150 112 recnd φ n A T + 1 A 1 n
151 78 149 150 fsummulc2 φ R n = A T + 1 A 1 n = n = A T + 1 A R 1 n
152 148 151 breqtrrd φ n = A T + 1 A B n R n = A T + 1 A 1 n
153 104 nnrecred φ n 1 A T 1 n
154 72 153 fsumrecl φ n = 1 A T 1 n
155 154 recnd φ n = 1 A T 1 n
156 113 recnd φ n = A T + 1 A 1 n
157 11 nnrecred φ n 1 A 1 n
158 157 recnd φ n 1 A 1 n
159 51 69 9 158 fsumsplit φ n = 1 A 1 n = n = 1 A T 1 n + n = A T + 1 A 1 n
160 155 156 159 mvrladdd φ n = 1 A 1 n n = 1 A T 1 n = n = A T + 1 A 1 n
161 9 157 fsumrecl φ n = 1 A 1 n
162 161 adantr φ A < 1 n = 1 A 1 n
163 154 adantr φ A < 1 n = 1 A T 1 n
164 162 163 resubcld φ A < 1 n = 1 A 1 n n = 1 A T 1 n
165 0red φ A < 1 0
166 31 adantr φ A < 1 log T + 1
167 fzfid φ A < 1 1 A T Fin
168 105 adantlr φ A < 1 n 1 A T n +
169 168 rpreccld φ A < 1 n 1 A T 1 n +
170 169 rpred φ A < 1 n 1 A T 1 n
171 169 rpge0d φ A < 1 n 1 A T 0 1 n
172 1 adantr φ A < 1 A +
173 172 rpge0d φ A < 1 0 A
174 simpr φ A < 1 A < 1
175 0p1e1 0 + 1 = 1
176 174 175 breqtrrdi φ A < 1 A < 0 + 1
177 57 adantr φ A < 1 A
178 0z 0
179 flbi A 0 A = 0 0 A A < 0 + 1
180 177 178 179 sylancl φ A < 1 A = 0 0 A A < 0 + 1
181 173 176 180 mpbir2and φ A < 1 A = 0
182 181 oveq2d φ A < 1 1 A = 1 0
183 fz10 1 0 =
184 182 183 eqtrdi φ A < 1 1 A =
185 0ss 1 A T
186 184 185 eqsstrdi φ A < 1 1 A 1 A T
187 167 170 171 186 fsumless φ A < 1 n = 1 A 1 n n = 1 A T 1 n
188 162 163 suble0d φ A < 1 n = 1 A 1 n n = 1 A T 1 n 0 n = 1 A 1 n n = 1 A T 1 n
189 187 188 mpbird φ A < 1 n = 1 A 1 n n = 1 A T 1 n 0
190 22 27 logge0d φ 0 log T
191 0le1 0 1
192 191 a1i φ 0 1
193 30 24 190 192 addge0d φ 0 log T + 1
194 193 adantr φ A < 1 0 log T + 1
195 164 165 166 189 194 letrd φ A < 1 n = 1 A 1 n n = 1 A T 1 n log T + 1
196 harmonicubnd A 1 A n = 1 A 1 n log A + 1
197 57 196 sylan φ 1 A n = 1 A 1 n log A + 1
198 harmoniclbnd A T + log A T n = 1 A T 1 n
199 44 198 syl φ log A T n = 1 A T 1 n
200 199 adantr φ 1 A log A T n = 1 A T 1 n
201 1 relogcld φ log A
202 peano2re log A log A + 1
203 201 202 syl φ log A + 1
204 44 relogcld φ log A T
205 le2sub n = 1 A 1 n n = 1 A T 1 n log A + 1 log A T n = 1 A 1 n log A + 1 log A T n = 1 A T 1 n n = 1 A 1 n n = 1 A T 1 n log A + 1 - log A T
206 161 154 203 204 205 syl22anc φ n = 1 A 1 n log A + 1 log A T n = 1 A T 1 n n = 1 A 1 n n = 1 A T 1 n log A + 1 - log A T
207 206 adantr φ 1 A n = 1 A 1 n log A + 1 log A T n = 1 A T 1 n n = 1 A 1 n n = 1 A T 1 n log A + 1 - log A T
208 197 200 207 mp2and φ 1 A n = 1 A 1 n n = 1 A T 1 n log A + 1 - log A T
209 201 recnd φ log A
210 24 recnd φ 1
211 30 recnd φ log T
212 209 210 211 pnncand φ log A + 1 - log A log T = 1 + log T
213 1 29 relogdivd φ log A T = log A log T
214 213 oveq2d φ log A + 1 - log A T = log A + 1 - log A log T
215 ax-1cn 1
216 addcom log T 1 log T + 1 = 1 + log T
217 211 215 216 sylancl φ log T + 1 = 1 + log T
218 212 214 217 3eqtr4d φ log A + 1 - log A T = log T + 1
219 218 adantr φ 1 A log A + 1 - log A T = log T + 1
220 208 219 breqtrd φ 1 A n = 1 A 1 n n = 1 A T 1 n log T + 1
221 195 220 57 24 ltlecasei φ n = 1 A 1 n n = 1 A T 1 n log T + 1
222 160 221 eqbrtrrd φ n = A T + 1 A 1 n log T + 1
223 lemul2a n = A T + 1 A 1 n log T + 1 R 0 R n = A T + 1 A 1 n log T + 1 R n = A T + 1 A 1 n R log T + 1
224 113 31 3 222 223 syl31anc φ R n = A T + 1 A 1 n R log T + 1
225 83 114 32 152 224 letrd φ n = A T + 1 A B n R log T + 1
226 77 83 20 32 110 225 le2addd φ n = 1 A T B n + n = A T + 1 A B n n = 1 A C + R log T + 1
227 71 226 eqbrtrd φ n = 1 A B n n = 1 A C + R log T + 1
228 16 19 33 43 227 letrd φ n = 1 A B n n = 1 A C + R log T + 1