Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem26 Structured version   Unicode version

Theorem stoweidlem26 31326
 Description: This lemma is used to prove that there is a function as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here is used to represnt j in the paper, is used to represent A in the paper, is used to represent t, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem26.1
stoweidlem26.2
stoweidlem26.3
stoweidlem26.4
stoweidlem26.5
stoweidlem26.6
stoweidlem26.7
stoweidlem26.8
stoweidlem26.9
stoweidlem26.10
stoweidlem26.11
stoweidlem26.12
stoweidlem26.13
stoweidlem26.14
stoweidlem26.15
Assertion
Ref Expression
stoweidlem26
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,   ,   ,,   ,
Allowed substitution hints:   (,)   (,,)   (,,)   ()   ()   (,)   (,)

Proof of Theorem stoweidlem26
StepHypRef Expression
1 1re 9591 . . . . . . . 8
2 eleq1 2539 . . . . . . . 8
31, 2mpbiri 233 . . . . . . 7
43adantl 466 . . . . . 6
5 4re 10608 . . . . . . . 8
65a1i 11 . . . . . . 7
7 3re 10605 . . . . . . . 8
87a1i 11 . . . . . . 7
9 3ne0 10626 . . . . . . . 8
109a1i 11 . . . . . . 7
116, 8, 10redivcld 10368 . . . . . 6
124, 11resubcld 9983 . . . . 5
13 stoweidlem26.11 . . . . . . 7
1413rpred 11252 . . . . . 6
1514adantr 465 . . . . 5
1612, 15remulcld 9620 . . . 4
17 0red 9593 . . . 4
18 fzfid 12047 . . . . . 6
1914adantr 465 . . . . . . 7
20 stoweidlem26.13 . . . . . . . 8
21 stoweidlem26.9 . . . . . . . . . . . . . 14
22 eldif 3486 . . . . . . . . . . . . . 14
2321, 22sylib 196 . . . . . . . . . . . . 13
2423simpld 459 . . . . . . . . . . . 12
25 1e0p1 11000 . . . . . . . . . . . . . . . 16
2625oveq1i 6292 . . . . . . . . . . . . . . 15
27 0z 10871 . . . . . . . . . . . . . . . 16
28 fzp1ss 11727 . . . . . . . . . . . . . . . 16
2927, 28ax-mp 5 . . . . . . . . . . . . . . 15
3026, 29eqsstri 3534 . . . . . . . . . . . . . 14
31 stoweidlem26.8 . . . . . . . . . . . . . 14
3230, 31sseldi 3502 . . . . . . . . . . . . 13
33 stoweidlem26.7 . . . . . . . . . . . . . 14
34 rabexg 4597 . . . . . . . . . . . . . 14
3533, 34syl 16 . . . . . . . . . . . . 13
36 oveq1 6289 . . . . . . . . . . . . . . . . 17
3736oveq1d 6297 . . . . . . . . . . . . . . . 16
3837breq2d 4459 . . . . . . . . . . . . . . 15
3938rabbidv 3105 . . . . . . . . . . . . . 14
40 stoweidlem26.4 . . . . . . . . . . . . . 14
4139, 40fvmptg 5946 . . . . . . . . . . . . 13
4232, 35, 41syl2anc 661 . . . . . . . . . . . 12
4324, 42eleqtrd 2557 . . . . . . . . . . 11
44 nfcv 2629 . . . . . . . . . . . 12
45 nfcv 2629 . . . . . . . . . . . 12
46 stoweidlem26.1 . . . . . . . . . . . . . 14
4746, 44nffv 5871 . . . . . . . . . . . . 13
48 nfcv 2629 . . . . . . . . . . . . 13
49 nfcv 2629 . . . . . . . . . . . . 13
5047, 48, 49nfbr 4491 . . . . . . . . . . . 12
51 fveq2 5864 . . . . . . . . . . . . 13
5251breq1d 4457 . . . . . . . . . . . 12
5344, 45, 50, 52elrabf 3259 . . . . . . . . . . 11
5443, 53sylib 196 . . . . . . . . . 10
5554simpld 459 . . . . . . . . 9
5655adantr 465 . . . . . . . 8
5720, 56ffvelrnd 6020 . . . . . . 7
5819, 57remulcld 9620 . . . . . 6
5918, 58fsumrecl 13515 . . . . 5
6059adantr 465 . . . 4
615, 7, 9redivcli 10307 . . . . . . 7
6261a1i 11 . . . . . 6
634, 62resubcld 9983 . . . . 5
644recnd 9618 . . . . . . . 8
6564subid1d 9915 . . . . . . 7
66 3cn 10606 . . . . . . . . . 10
6766, 9dividi 10273 . . . . . . . . 9
68 3lt4 10701 . . . . . . . . . 10
69 3pos 10625 . . . . . . . . . . 11
707, 5, 7, 69ltdiv1ii 10471 . . . . . . . . . 10
7168, 70mpbi 208 . . . . . . . . 9
7267, 71eqbrtrri 4468 . . . . . . . 8
73 breq1 4450 . . . . . . . . 9
7473adantl 466 . . . . . . . 8
7572, 74mpbiri 233 . . . . . . 7
7665, 75eqbrtrd 4467 . . . . . 6
774, 17, 62, 76ltsub23d 10153 . . . . 5
7813rpgt0d 11255 . . . . . 6
7978adantr 465 . . . . 5
80 mulltgt0 30975 . . . . 5
8163, 77, 15, 79, 80syl22anc 1229 . . . 4
82 0cn 9584 . . . . . . . 8
83 fsumconst 13564 . . . . . . . 8
8418, 82, 83sylancl 662 . . . . . . 7
85 hashcl 12392 . . . . . . . . 9
86 nn0cn 10801 . . . . . . . . 9
8718, 85, 863syl 20 . . . . . . . 8
8887mul01d 9774 . . . . . . 7
8984, 88eqtrd 2508 . . . . . 6
9089adantr 465 . . . . 5
91 0red 9593 . . . . . . 7
9213rpge0d 11256 . . . . . . . . 9
9392adantr 465 . . . . . . . 8
94 stoweidlem26.3 . . . . . . . . . . . 12
95 nfv 1683 . . . . . . . . . . . 12
9694, 95nfan 1875 . . . . . . . . . . 11
97 nfv 1683 . . . . . . . . . . 11
9896, 97nfim 1867 . . . . . . . . . 10
99 fveq2 5864 . . . . . . . . . . . 12
10099breq2d 4459 . . . . . . . . . . 11
101100imbi2d 316 . . . . . . . . . 10
102 stoweidlem26.14 . . . . . . . . . . . 12
1031023expia 1198 . . . . . . . . . . 11
104103com12 31 . . . . . . . . . 10
10544, 98, 101, 104vtoclgaf 3176 . . . . . . . . 9
10656, 105mpcom 36 . . . . . . . 8
10719, 57, 93, 106mulge0d 10125 . . . . . . 7
10818, 91, 58, 107fsumle 13572 . . . . . 6
109108adantr 465 . . . . 5
11090, 109eqbrtrrd 4469 . . . 4
11116, 17, 60, 81, 110ltletrd 9737 . . 3
112 elfzelz 11684 . . . . . . . . 9
113 zre 10864 . . . . . . . . 9
11431, 112, 1133syl 20 . . . . . . . 8
1155a1i 11 . . . . . . . . 9
1167a1i 11 . . . . . . . . 9
1179a1i 11 . . . . . . . . 9
118115, 116, 117redivcld 10368 . . . . . . . 8
119114, 118resubcld 9983 . . . . . . 7
120119, 14remulcld 9620 . . . . . 6
121120adantr 465 . . . . 5
1221a1i 11 . . . . . . . . 9
123 stoweidlem26.6 . . . . . . . . . 10
12414, 123nndivred 10580 . . . . . . . . 9
125122, 124resubcld 9983 . . . . . . . 8
126114, 122resubcld 9983 . . . . . . . 8
127125, 126remulcld 9620 . . . . . . 7
12814, 127remulcld 9620 . . . . . 6
129128adantr 465 . . . . 5
130 fzfid 12047 . . . . . . . 8
13131, 112syl 16 . . . . . . . . . . . . . 14
132 2z 10892 . . . . . . . . . . . . . . 15
133132a1i 11 . . . . . . . . . . . . . 14
134131, 133zsubcld 10967 . . . . . . . . . . . . 13
135123nnzd 10961 . . . . . . . . . . . . 13
136131zred 10962 . . . . . . . . . . . . . . 15
137 2re 10601 . . . . . . . . . . . . . . . 16
138137a1i 11 . . . . . . . . . . . . . . 15
139136, 138resubcld 9983 . . . . . . . . . . . . . 14
140123nnred 10547 . . . . . . . . . . . . . 14
141 0le2 10622 . . . . . . . . . . . . . . . 16
142 0red 9593 . . . . . . . . . . . . . . . . 17
143142, 138, 136lesub2d 10156 . . . . . . . . . . . . . . . 16
144141, 143mpbii 211 . . . . . . . . . . . . . . 15
145131zcnd 10963 . . . . . . . . . . . . . . . 16
146145subid1d 9915 . . . . . . . . . . . . . . 15
147144, 146breqtrd 4471 . . . . . . . . . . . . . 14
148 elfzle2 11686 . . . . . . . . . . . . . . 15
14931, 148syl 16 . . . . . . . . . . . . . 14
150139, 136, 140, 147, 149letrd 9734 . . . . . . . . . . . . 13
151134, 135, 1503jca 1176 . . . . . . . . . . . 12
152 eluz2 11084 . . . . . . . . . . . 12
153151, 152sylibr 212 . . . . . . . . . . 11
154 fzss2 11719 . . . . . . . . . . 11
155153, 154syl 16 . . . . . . . . . 10
156155sselda 3504 . . . . . . . . 9
157156, 57syldan 470 . . . . . . . 8
158130, 157fsumrecl 13515 . . . . . . 7
15914, 158remulcld 9620 . . . . . 6
160159adantr 465 . . . . 5
16114, 126remulcld 9620 . . . . . . . . 9
16214, 14remulcld 9620 . . . . . . . . 9
163161, 162resubcld 9983 . . . . . . . 8
164126, 123nndivred 10580 . . . . . . . . . 10
165162, 164remulcld 9620 . . . . . . . . 9
166161, 165resubcld 9983 . . . . . . . 8
167126, 14resubcld 9983 . . . . . . . . . 10
168122, 14readdcld 9619 . . . . . . . . . . . 12
1691, 7, 9redivcli 10307 . . . . . . . . . . . . . . 15
170169a1i 11 . . . . . . . . . . . . . 14
171 stoweidlem26.12 . . . . . . . . . . . . . 14
17214, 170, 122, 171ltadd2dd 9736 . . . . . . . . . . . . 13
173 ax-1cn 9546 . . . . . . . . . . . . . . 15
17466, 173, 66, 9divdiri 10297 . . . . . . . . . . . . . 14
175 3p1e4 10657 . . . . . . . . . . . . . . 15
176175oveq1i 6292 . . . . . . . . . . . . . 14
17767oveq1i 6292 . . . . . . . . . . . . . 14
178174, 176, 1773eqtr3ri 2505 . . . . . . . . . . . . 13
179172, 178syl6breq 4486 . . . . . . . . . . . 12
180168, 118, 114, 179ltsub2dd 10161 . . . . . . . . . . 11
181173a1i 11 . . . . . . . . . . . 12
18213rpcnd 11254 . . . . . . . . . . . 12
183145, 181, 182subsub4d 9957 . . . . . . . . . . 11
184180, 183breqtrrd 4473 . . . . . . . . . 10
185119, 167, 13, 184ltmul1dd 11303 . . . . . . . . 9
186145, 181subcld 9926 . . . . . . . . . . . 12
187186, 182subcld 9926 . . . . . . . . . . 11
188182, 187mulcomd 9613 . . . . . . . . . 10
189182, 186, 182subdid 10008 . . . . . . . . . 10
190188, 189eqtr3d 2510 . . . . . . . . 9
191185, 190breqtrd 4471 . . . . . . . 8
192 1zzd 10891 . . . . . . . . . . . . . . . . 17
193 elfz 11674 . . . . . . . . . . . . . . . . 17
194131, 192, 135, 193syl3anc 1228 . . . . . . . . . . . . . . . 16
19531, 194mpbid 210 . . . . . . . . . . . . . . 15
196195simprd 463 . . . . . . . . . . . . . 14
197 zlem1lt 10910 . . . . . . . . . . . . . . 15
198131, 135, 197syl2anc 661 . . . . . . . . . . . . . 14
199196, 198mpbid 210 . . . . . . . . . . . . 13
200123nngt0d 10575 . . . . . . . . . . . . . 14
201 ltdiv1 10402 . . . . . . . . . . . . . 14
202126, 140, 140, 200, 201syl112anc 1232 . . . . . . . . . . . . 13
203199, 202mpbid 210 . . . . . . . . . . . 12
204123nncnd 10548 . . . . . . . . . . . . 13
205123nnne0d 10576 . . . . . . . . . . . . 13
206204, 205dividd 10314 . . . . . . . . . . . 12
207203, 206breqtrd 4471 . . . . . . . . . . 11
20814, 14, 78, 78mulgt0d 9732 . . . . . . . . . . . 12
209 ltmul2 10389 . . . . . . . . . . . 12
210164, 122, 162, 208, 209syl112anc 1232 . . . . . . . . . . 11
211207, 210mpbid 210 . . . . . . . . . 10
212182, 182mulcld 9612 . . . . . . . . . . 11
213212mulid1d 9609 . . . . . . . . . 10
214211, 213breqtrd 4471 . . . . . . . . 9
215165, 162, 161, 214ltsub2dd 10161 . . . . . . . 8
216120, 163, 166, 191, 215lttrd 9738 . . . . . . 7
217182, 204, 205divcld 10316 . . . . . . . . . . 11
218181, 217, 186subdird 10009 . . . . . . . . . 10
219186mulid2d 9610 . . . . . . . . . . 11
220219oveq1d 6297 . . . . . . . . . 10
221218, 220eqtrd 2508 . . . . . . . . 9
222221oveq2d 6298 . . . . . . . 8
223217, 186mulcld 9612 . . . . . . . . 9
224182, 186, 223subdid 10008 . . . . . . . 8
225182, 204, 186, 205div32d 10339 . . . . . . . . . . 11
226225oveq2d 6298 . . . . . . . . . 10
227186, 204, 205divcld 10316 . . . . . . . . . . 11
228182, 182, 227mulassd 9615 . . . . . . . . . 10
229226, 228eqtr4d 2511 . . . . . . . . 9
230229oveq2d 6298 . . . . . . . 8
231222, 224, 2303eqtrd 2512 . . . . . . 7
232216, 231breqtrrd 4473 . . . . . 6
233232adantr 465 . . . . 5
234181, 217subcld 9926 . . . . . . . . . 10
235 fsumconst 13564 . . . . . . . . . 10
236130, 234, 235syl2anc 661 . . . . . . . . 9
237236adantr 465 . . . . . . . 8
238 0zd 10872 . . . . . . . . . . . . 13
23931adantr 465 . . . . . . . . . . . . . . 15
240239, 112syl 16 . . . . . . . . . . . . . 14
241132a1i 11 . . . . . . . . . . . . . 14
242240, 241zsubcld 10967 . . . . . . . . . . . . 13
243 elnnuz 11114 . . . . . . . . . . . . . . . . . . . 20
244123, 243sylib 196 . . . . . . . . . . . . . . . . . . 19
245 elfzp12 11753 . . . . . . . . . . . . . . . . . . 19
246244, 245syl 16 . . . . . . . . . . . . . . . . . 18
24731, 246mpbid 210 . . . . . . . . . . . . . . . . 17
248247orcanai 911 . . . . . . . . . . . . . . . 16
249 1p1e2 10645 . . . . . . . . . . . . . . . . . 18
250249a1i 11 . . . . . . . . . . . . . . . . 17
251250oveq1d 6297 . . . . . . . . . . . . . . . 16
252248, 251eleqtrd 2557 . . . . . . . . . . . . . . 15
253 elfzle1 11685 . . . . . . . . . . . . . . 15
254252, 253syl 16 . . . . . . . . . . . . . 14
255114adantr 465 . . . . . . . . . . . . . . 15
256137a1i 11 . . . . . . . . . . . . . . 15
257255, 256subge0d 10138 . . . . . . . . . . . . . 14
258254, 257mpbird 232 . . . . . . . . . . . . 13
259238, 242, 2583jca 1176 . . . . . . . . . . . 12
260 eluz2 11084 . . . . . . . . . . . 12
261259, 260sylibr 212 . . . . . . . . . . 11
262 hashfz 12446 . . . . . . . . . . 11
263261, 262syl 16 . . . . . . . . . 10
264 2cn 10602 . . . . . . . . . . . . . . . 16
265264a1i 11 . . . . . . . . . . . . . . 15
266145, 265subcld 9926 . . . . . . . . . . . . . 14
267266subid1d 9915 . . . . . . . . . . . . 13
268267oveq1d 6297 . . . . . . . . . . . 12
269145, 265, 181subadd23d 9948 . . . . . . . . . . . 12
270264, 173negsubdi2i 9901 . . . . . . . . . . . . . . . 16
271 2m1e1 10646 . . . . . . . . . . . . . . . . 17
272271negeqi 9809 . . . . . . . . . . . . . . . 16
273270, 272eqtr3i 2498 . . . . . . . . . . . . . . 15
274273a1i 11 . . . . . . . . . . . . . 14
275274oveq2d 6298 . . . . . . . . . . . . 13
276145, 181negsubd 9932 . . . . . . . . . . . . 13
277275, 276eqtrd 2508 . . . . . . . . . . . 12
278268, 269, 2773eqtrd 2512 . . . . . . . . . . 11
279278adantr 465 . . . . . . . . . 10
280263, 279eqtrd 2508 . . . . . . . . 9
281280oveq1d 6297 . . . . . . . 8
282186, 234mulcomd 9613 . . . . . . . . 9
283282adantr 465 . . . . . . . 8
284237, 281, 2833eqtrd 2512 . . . . . . 7
285 fzfid 12047 . . . . . . . 8
286 fzn0 11696 . . . . . . . . 9
287261, 286sylibr 212 . . . . . . . 8
288125ad2antrr 725 . . . . . . . 8
289 simpll 753 . . . . . . . . 9
290156adantlr 714 . . . . . . . . 9
291289, 290, 57syl2anc 661 . . . . . . . 8
29255adantr 465 . . . . . . . . . . . 12
293 elfzelz 11684 . . . . . . . . . . . . . . . . 17
294293zred 10962 . . . . . . . . . . . . . . . 16
295294adantl 466 . . . . . . . . . . . . . . 15
296169a1i 11 . . . . . . . . . . . . . . 15
297295, 296readdcld 9619 . . . . . . . . . . . . . 14
29814adantr 465 . . . . . . . . . . . . . 14
299297, 298remulcld 9620 . . . . . . . . . . . . 13
300114adantr 465 . . . . . . . . . . . . . . . 16
301137a1i 11 . . . . . . . . . . . . . . . 16
302300, 301resubcld 9983 . . . . . . . . . . . . . . 15
303302, 296readdcld 9619 . . . . . . . . . . . . . 14
304303, 298remulcld 9620 . . . . . . . . . . . . 13
305 stoweidlem26.10 . . . . . . . . . . . . . . . 16
306305, 55jca 532 . . . . . . . . . . . . . . 15
307306adantr 465 . . . . . . . . . . . . . 14
308 ffvelrn 6017 . . . . . . . . . . . . . 14
309307, 308syl 16 . . . . . . . . . . . . 13
310 elfzle2 11686 . . . . . . . . . . . . . . . 16
311310adantl 466 . . . . . . . . . . . . . . 15
312295, 302, 296, 311leadd1dd 10162 . . . . . . . . . . . . . 14
31314, 78jca 532 . . . . . . . . . . . . . . . 16
314313adantr 465 . . . . . . . . . . . . . . 15
315 lemul1 10390 . . . . . . . . . . . . . . 15
316297, 303, 314, 315syl3anc 1228 . . . . . . . . . . . . . 14
317312, 316mpbid 210 . . . . . . . . . . . . 13
318114, 138resubcld 9983 . . . . . . . . . . . . . . . . 17
319318, 170readdcld 9619 . . . . . . . . . . . . . . . 16
320319, 14remulcld 9620 . . . . . . . . . . . . . . 15
321305, 55ffvelrnd 6020 . . . . . . . . . . . . . . 15
322126, 170resubcld 9983 . . . . . . . . . . . . . . . . 17
323322, 14remulcld 9620 . . . . . . . . . . . . . . . 16
324 addid1 9755 . . . . . . . . . . . . . . . . . . . . . . . . 25
325324eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24
326173, 325mp1i 12 . . . . . . . . . . . . . . . . . . . . . . 23
327181subidd 9914 . . . . . . . . . . . . . . . . . . . . . . . . 25
328327eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24
329328oveq2d 6298 . . . . . . . . . . . . . . . . . . . . . . 23
330 addsubass 9826 . . . . . . . . . . . . . . . . . . . . . . . . 25
331330eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . 24
332181, 181, 181, 331syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . 23
333326, 329, 3323eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . 22
334333oveq2d 6298 . . . . . . . . . . . . . . . . . . . . 21
335249a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
336335oveq1d 6297 . . . . . . . . . . . . . . . . . . . . . 22
337336oveq2d 6298 . . . . . . . . . . . . . . . . . . . . 21
338145, 265, 181subsubd 9954 . . . . . . . . . . . . . . . . . . . . 21
339334, 337, 3383eqtrd 2512 . . . . . . . . . . . . . . . . . . . 20
340339oveq1d 6297 . . . . . . . . . . . . . . . . . . 19
341264, 66, 9divcli 10282 . . . . . . . . . . . . . . . . . . . . 21
342341a1i 11 . . . . . . . . . . . . . . . . . . . 20
343266, 181, 342addsubassd 9946 . . . . . . . . . . . . . . . . . . 19
344173, 66, 9divcli 10282 . . . . . . . . . . . . . . . . . . . . . 22
345 df-3 10591 . . . . . . . . . . . . . . . . . . . . . . . 24
346345oveq1i 6292 . . . . . . . . . . . . . . . . . . . . . . 23
347264, 173, 66, 9divdiri 10297 . . . . . . . . . . . . . . . . . . . . . . 23
348346, 67, 3473eqtr3ri 2505 . . . . . . . . . . . . . . . . . . . . . 22
349173, 341, 344, 348subaddrii 9904 . . . . . . . . . . . . . . . . . . . . 21
350349a1i 11 . . . . . . . . . . . . . . . . . . . 20
351350oveq2d 6298 . . . . . . . . . . . . . . . . . . 19
352340, 343, 3513eqtrd 2512 . . . . . . . . . . . . . . . . . 18
353137, 7, 9redivcli 10307 . . . . . . . . . . . . . . . . . . . 20
354353a1i 11 . . . . . . . . . . . . . . . . . . 19
355 1lt2 10698 . . . . . . . . . . . . . . . . . . . 20
3567, 69pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . 22
3571, 137, 3563pm3.2i 1174 . . . . . . . . . . . . . . . . . . . . 21
358 ltdiv1 10402 . . . . . . . . . . . . . . . . . . . . 21
359357, 358mp1i 12 . . . . . . . . . . . . . . . . . . . 20
360355, 359mpbii 211 . . . . . . . . . . . . . . . . . . 19
361170, 354, 126, 360ltsub2dd 10161 . . . . . . . . . . . . . . . . . 18
362352, 361eqbrtrrd 4469 . . . . . . . . . . . . . . . . 17
363319, 322, 13, 362ltmul1dd 11303 . . . . . . . . . . . . . . . 16
36423simprd 463 . . . . . . . . . . . . . . . . . . . . . . 23
365195simpld 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
366140, 122readdcld 9619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
367140lep1d 10473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
368114, 140, 366, 196, 367letrd 9734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
369135peano2zd 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
370 elfz 11674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
371131, 192, 369, 370syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
372365, 368, 371mpbir2and 920 . . . . . . . . . . . . . . . . . . . . . . . . . 26
373145, 181npcand 9930 . . . . . . . . . . . . . . . . . . . . . . . . . 26
374 0p1e1 10643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
375374a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
376375oveq1d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . 26
377372, 373, 3763eltr4d 2570 . . . . . . . . . . . . . . . . . . . . . . . . 25
378 0zd 10872 . . . . . . . . . . . . . . . . . . . . . . . . . 26
379131, 192zsubcld 10967 . . . . . . . . . . . . . . . . . . . . . . . . . 26
380 fzaddel 11714 . . . . . . . . . . . . . . . . . . . . . . . . . 26
381378, 135, 379, 192, 380syl22anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . 25
382377, 381mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24
383 rabexg 4597 . . . . . . . . . . . . . . . . . . . . . . . . 25
38433, 383syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
385 oveq1 6289 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
386385oveq1d 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
387386breq2d 4459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
388387rabbidv 3105 . . . . . . . . . . . . . . . . . . . . . . . . 25
389388, 40fvmptg 5946 . . . . . . . . . . . . . . . . . . . . . . . 24
390382, 384, 389syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
391364, 390neleqtrd 2579 . . . . . . . . . . . . . . . . . . . . . 22
392 nfcv 2629 . . . . . . . . . . . . . . . . . . . . . . . 24
39347, 48, 392nfbr 4491 . . . . . . . . . . . . . . . . . . . . . . 23
39451breq1d 4457 . . . . . . . . . . . . . . . . . . . . . . 23
39544, 45, 393, 394elrabf 3259 . . . . . . . . . . . . . . . . . . . . . 22
396391, 395sylnib 304 . . . . . . . . . . . . . . . . . . . . 21
397 ianor 488 . . . . . . . . . . . . . . . . . . . . 21
398396, 397sylib 196 . . . . . . . . . . . . . . . . . . . 20
399 olc 384 . . . . . . . . . . . . . . . . . . . . 21
400399anim1i 568 . . . . . . . . . . . . . . . . . . . 20
40155, 398, 400syl2anc 661 . . . . . . . . . . . . . . . . . . 19
402 orcom 387 . . . . . . . . . . . . . . . . . . . 20
403402anbi2i 694 . . . . . . . . . . . . . . . . . . 19
404401, 403sylib 196 . . . . . . . . . . . . . . . . . 18
405 pm4.43 925 . . . . . . . . . . . . . . . . . 18
406404, 405sylibr 212 . . . . . . . . . . . . . . . . 17
407323, 321ltnled 9727 . . . . . . . . . . . . . . . . 17
408406, 407mpbird 232 . . . . . . . . . . . . . . . 16
409320, 323, 321, 363, 408lttrd 9738 . . . . . . . . . . . . . . 15
410320, 321, 409ltled 9728 . . . . . . . . . . . . . 14
411410adantr 465 . . . . . . . . . . . . 13
412299, 304, 309, 317, 411letrd 9734 . . . . . . . . . . . 12
413 nfcv 2629 . . . . . . . . . . . . . 14
414413, 48, 47nfbr 4491 . . . . . . . . . . . . 13
41551breq2d 4459 . . . . . . . . . . . . 13
41644, 45, 414, 415elrabf 3259 . . . . . . . . . . . 12
417292, 412, 416sylanbrc 664 . . . . . . . . . . 11
418 rabexg 4597 . . . . . . . . . . . . . 14
41933, 418syl 16 . . . . . . . . . . . . 13
420419adantr 465 . . . . . . . . . . . 12
421 oveq1 6289 . . . . . . . . . . . . . . . 16
422421oveq1d 6297 . . . . . . . . . . . . . . 15
423422breq1d 4457 . . . . . . . . . . . . . 14
424423rabbidv 3105 . . . . . . . . . . . . 13
425 stoweidlem26.5 . . . . . . . . . . . . 13
426424, 425fvmptg 5946 . . . . . . . . . . . 12
427156, 420, 426syl2anc 661 . . . . . . . . . . 11
428417, 427eleqtrrd 2558 . . . . . . . . . 10
4291513ad2ant1 1017 . . . . . . . . . . . . . 14
430429, 152sylibr 212 . . . . . . . . . . . . 13
431430, 154syl 16 . . . . . . . . . . . 12
432 simp2 997 . . . . . . . . . . . 12
433431, 432sseldd 3505 . . . . . . . . . . 11
434 elex 3122 . . . . . . . . . . . . 13
4354343ad2ant3 1019 . . . . . . . . . . . 12
436 nfcv 2629 . . . . . . . . . . . . . . . . . . 19
437 nfrab1 3042 . . . . . . . . . . . . . . . . . . 19
438436, 437nfmpt 4535 . . . . . . . . . . . . . . . . . 18
439425, 438nfcxfr 2627 . . . . . . . . . . . . . . . . 17
440 nfcv 2629 . . . . . . . . . . . . . . . . 17
441439, 440nffv 5871 . . . . . . . . . . . . . . . 16
442441nfel2 2647 . . . . . . . . . . . . . . 15
44394, 95, 442nf3an 1877 . . . . . . . . . . . . . 14
444 nfv 1683 . . . . . . . . . . . . . 14
445443, 444nfim 1867 . . . . . . . . . . . . 13
446 eleq1 2539 . . . . . . . . . . . . . . 15
4474463anbi3d 1305 . . . . . . . . . . . . . 14
44899breq2d 4459 . . . . . . . . . . . . . 14
449447, 448imbi12d 320 . . . . . . . . . . . . 13
450 stoweidlem26.15 . . . . . . . . . . . . 13
451445, 449, 450vtoclg1f 3170 . . . . . . . . . . . 12
452435, 451mpcom 36 . . . . . . . . . . 11
453433, 452syld3an2 1275 . . . . . . . . . 10
454428, 453mpd3an3 1325 . . . . . . . . 9
455454adantlr 714 . . . . . . . 8
456285, 287, 288, 291, 455fsumlt 13573 . . . . . . 7
457284, 456eqbrtrrd 4469 . . . . . 6
458127adantr 465 . . . . . . 7
459158adantr 465 . . . . . . 7
460313adantr 465 . . . . . . 7
461 ltmul2 10389 . . . . . . 7
462458, 459, 460, 461syl3anc 1228 . . . . . 6
463457, 462mpbid 210 . . . . 5
464121, 129, 160, 233, 463lttrd 9738 . . . 4
465156, 58syldan 470 . . . . . . . . . 10
466465adantlr 714 . . . . . . . . 9
467466recnd 9618 . . . . . . . 8
468285, 467fsumcl 13514 . . . . . . 7
469468addid1d 9775 . . . . . 6
470 0red 9593 . . . . . . 7
471 fzfid 12047 . . . . . . . 8
47214adantr 465 . . . . . . . . . 10
473 0red 9593 . . . . . . . . . . . . 13
474126adantr 465 . . . . . . . . . . . . 13
475 elfzelz 11684 . . . . . . . . . . . . . . 15
476475zred 10962 . . . . . . . . . . . . . 14
477476adantl 466 . . . . . . . . . . . . 13
478 1m1e0 10600 . . . . . . . . . . . . . . 15
479122, 114, 122, 365lesub1dd 10164 . . . . . . . . . . . . . . 15
480478, 479syl5eqbrr 4481 . . . . . . . . . . . . . 14
481480adantr 465 . . . . . . . . . . . . 13
482 simpr 461 . . . . . . . . . . . . . . 15
483475adantl 466 . . . . . . . . . . . . . . . 16
484379adantr 465 . . . . . . . . . . . . . . . 16
485135adantr 465 . . . . . . . . . . . . . . . 16
486 elfz 11674 . . . . . . . . . . . . . . . 16
487483, 484, 485, 486syl3anc 1228 . . . . . . . . . . . . . . 15
488482, 487mpbid 210 . . . . . . . . . . . . . 14
489488simpld 459 . . . . . . . . . . . . 13
490473, 474, 477, 481, 489letrd 9734 . . . . . . . . . . . 12
491 elfzle2 11686 . . . . . . . . . . . . 13
492491adantl 466 . . . . . . . . . . . 12
493 0zd 10872 . . . . . . . . . . . . 13
494 elfz 11674 . . . . . . . . . . . . 13
495483, 493, 485, 494syl3anc 1228 . . . . . . . . . . . 12
496490, 492, 495mpbir2and 920 . . . . . . . . . . 11
497496, 57syldan 470 . . . . . . . . . 10
498472, 497remulcld 9620 . . . . . . . . 9
499498adantlr 714 . . . . . . . 8
500471, 499fsumrecl 13515 . . . . . . 7
501285, 466fsumrecl 13515 . . . . . . 7
502 fzfid 12047 . . . . . . . . 9
503182adantr 465 . . . . . . . . . . 11
504503mul01d 9774 . . . . . . . . . 10
505496, 106syldan 470 . . . . . . . . . . 11
506313adantr 465 . . . . . . . . . . . 12
507 lemul2 10391 . . . . . . . . . . . 12
508473, 497, 506, 507syl3anc 1228 . . . . . . . . . . 11
509505, 508mpbid 210 . . . . . . . . . 10
510504, 509eqbrtrrd 4469 . . . . . . . . 9
511502, 498, 510fsumge0 13568 . . . . . . . 8
512511adantr 465 . . . . . . 7
513470, 500, 501, 512leadd2dd 10163 . . . . . 6
514469, 513eqbrtrrd 4469 . . . . 5
515157recnd 9618 . . . . . . 7
516130, 182, 515fsummulc2 13558 . . . . . 6
517516adantr 465 . . . . 5
518 stoweidlem26.2 . . . . . . . . 9
519 elfzelz 11684 . . . . . . . . . . . . . . . 16
520519adantl 466 . . . . . . . . . . . . . . 15
521520zred 10962 . . . . . . . . . . . . . 14
522318adantr 465 . . . . . . . . . . . . . 14
523126adantr 465 . . . . . . . . . . . . . 14
524 simpr 461 . . . . . . . . . . . . . . . 16
525 0zd 10872 . . . . . . . . . . . . . . . . 17
526134adantr 465 . . . . . . . . . . . . . . . . 17
527 elfz 11674 . . . . . . . . . . . . . . . . 17
528520, 525, 526, 527syl3anc 1228 . . . . . . . . . . . . . . . 16
529524, 528mpbid 210 . . . . . . . . . . . . . . 15
530529simprd 463 . . . . . . . . . . . . . 14
531122, 138, 114ltsub2d 10158 . . . . . . . . . . . . . . . 16
532355, 531mpbii 211 . . . . . . . . . . . . . . 15
533532adantr 465 . . . . . . . . . . . . . 14
534521, 522, 523, 530, 533lelttrd 9735 . . . . . . . . . . . . 13
535521, 523ltnled 9727 . . . . . . . . . . . . 13
536534, 535mpbid 210 . . . . . . . . . . . 12