Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvfsumlem3 Structured version   Unicode version

Theorem dvfsumlem3 19902
 Description: Lemma for dvfsumrlim 19905. (Contributed by Mario Carneiro, 17-May-2016.)
Hypotheses
Ref Expression
dvfsum.s
dvfsum.z
dvfsum.m
dvfsum.d
dvfsum.md
dvfsum.t
dvfsum.a
dvfsum.b1
dvfsum.b2
dvfsum.b3
dvfsum.c
dvfsum.u
dvfsum.l
dvfsum.h
dvfsumlem1.1
dvfsumlem1.2
dvfsumlem1.3
dvfsumlem1.4
dvfsumlem1.5
Assertion
Ref Expression
dvfsumlem3
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,   ,,   ,   ,,   ,,
Allowed substitution hints:   (,)   ()   ()   ()   (,)   (,)   ()

Proof of Theorem dvfsumlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . 4
2 ioossre 10962 . . . 4
31, 2eqsstri 3370 . . 3
4 dvfsumlem1.2 . . 3
53, 4sseldi 3338 . 2
6 dvfsumlem1.1 . . . 4
73, 6sseldi 3338 . . 3
8 reflcl 11195 . . 3
9 peano2re 9229 . . 3
107, 8, 93syl 19 . 2
11 dvfsum.z . . 3
12 dvfsum.m . . . 4
14 dvfsum.d . . . 4
16 dvfsum.md . . . 4
18 dvfsum.t . . . 4
20 dvfsum.a . . . 4
22 dvfsum.b1 . . . 4
24 dvfsum.b2 . . . 4
26 dvfsum.b3 . . . 4
28 dvfsum.c . . 3
29 dvfsum.u . . . 4
31 dvfsum.l . . . 4
33 dvfsum.h . . 3
36 dvfsumlem1.3 . . . 4
38 dvfsumlem1.4 . . . 4
40 dvfsumlem1.5 . . . 4
42 simpr 448 . . 3
431, 11, 13, 15, 17, 19, 21, 23, 25, 27, 28, 30, 32, 33, 34, 35, 37, 39, 41, 42dvfsumlem2 19901 . 2
443a1i 11 . . . . . . . . . . 11
4544sselda 3340 . . . . . . . . . 10
46 reflcl 11195 . . . . . . . . . . 11
4745, 46syl 16 . . . . . . . . . 10
4845, 47resubcld 9455 . . . . . . . . 9
4944, 20, 22, 26dvmptrecl 19898 . . . . . . . . 9
5048, 49remulcld 9106 . . . . . . . 8
51 fzfid 11302 . . . . . . . . . 10
5224ralrimiva 2781 . . . . . . . . . . . 12
5352adantr 452 . . . . . . . . . . 11
54 elfzuz 11045 . . . . . . . . . . . 12
5554, 11syl6eleqr 2526 . . . . . . . . . . 11
5628eleq1d 2501 . . . . . . . . . . . 12
5756rspccva 3043 . . . . . . . . . . 11
5853, 55, 57syl2an 464 . . . . . . . . . 10
5951, 58fsumrecl 12518 . . . . . . . . 9
6059, 20resubcld 9455 . . . . . . . 8
6150, 60readdcld 9105 . . . . . . 7
6261, 33fmptd 5885 . . . . . 6
6362adantr 452 . . . . 5
644adantr 452 . . . . 5
6563, 64ffvelrnd 5863 . . . 4
665adantr 452 . . . . . . . 8
67 reflcl 11195 . . . . . . . 8
6866, 67syl 16 . . . . . . 7
6918adantr 452 . . . . . . . 8
707adantr 452 . . . . . . . . 9
7170, 8, 93syl 19 . . . . . . . 8
726, 1syl6eleq 2525 . . . . . . . . . . . 12
7318rexrd 9124 . . . . . . . . . . . . 13
74 elioopnf 10988 . . . . . . . . . . . . 13
7573, 74syl 16 . . . . . . . . . . . 12
7672, 75mpbid 202 . . . . . . . . . . 11
7776simprd 450 . . . . . . . . . 10
78 fllep1 11200 . . . . . . . . . . 11
797, 78syl 16 . . . . . . . . . 10
8018, 7, 10, 77, 79ltletrd 9220 . . . . . . . . 9
8180adantr 452 . . . . . . . 8
82 simpr 448 . . . . . . . . 9
8370flcld 11197 . . . . . . . . . . 11
8483peano2zd 10368 . . . . . . . . . 10
85 flge 11204 . . . . . . . . . 10
8666, 84, 85syl2anc 643 . . . . . . . . 9
8782, 86mpbid 202 . . . . . . . 8
8869, 71, 68, 81, 87ltletrd 9220 . . . . . . 7
8973adantr 452 . . . . . . . 8
90 elioopnf 10988 . . . . . . . 8
9189, 90syl 16 . . . . . . 7
9268, 88, 91mpbir2and 889 . . . . . 6
9392, 1syl6eleqr 2526 . . . . 5
9463, 93ffvelrnd 5863 . . . 4
956adantr 452 . . . . 5
9663, 95ffvelrnd 5863 . . . 4
9712adantr 452 . . . . . 6
9814adantr 452 . . . . . 6
9916adantr 452 . . . . . 6
10020adantlr 696 . . . . . 6
10122adantlr 696 . . . . . 6
10224adantlr 696 . . . . . 6
10326adantr 452 . . . . . 6
10429adantr 452 . . . . . 6
105313adant1r 1177 . . . . . 6
10636adantr 452 . . . . . . . 8
10770, 78syl 16 . . . . . . . 8
10898, 70, 71, 106, 107letrd 9217 . . . . . . 7
10998, 71, 68, 108, 87letrd 9217 . . . . . 6
110 flle 11198 . . . . . . 7
11166, 110syl 16 . . . . . 6
11240adantr 452 . . . . . 6
113 fllep1 11200 . . . . . . . 8
11466, 113syl 16 . . . . . . 7
115 flidm 11207 . . . . . . . . 9
11666, 115syl 16 . . . . . . . 8
117116oveq1d 6088 . . . . . . 7
118114, 117breqtrrd 4230 . . . . . 6
1191, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 93, 64, 109, 111, 112, 118dvfsumlem2 19901 . . . . 5
120119simpld 446 . . . 4
121 elioopnf 10988 . . . . . . . . . 10
12273, 121syl 16 . . . . . . . . 9
12310, 80, 122mpbir2and 889 . . . . . . . 8
124123, 1syl6eleqr 2526 . . . . . . 7
125124adantr 452 . . . . . 6
12663, 125ffvelrnd 5863 . . . . 5
12766flcld 11197 . . . . . . 7
128 eluz2 10484 . . . . . . 7
12984, 127, 87, 128syl3anbrc 1138 . . . . . 6
13063adantr 452 . . . . . . 7
131 elfzelz 11049 . . . . . . . . . . 11
132131adantl 453 . . . . . . . . . 10
133132zred 10365 . . . . . . . . 9
13469adantr 452 . . . . . . . . . 10
13571adantr 452 . . . . . . . . . 10
13680ad2antrr 707 . . . . . . . . . 10
137 elfzle1 11050 . . . . . . . . . . 11
138137adantl 453 . . . . . . . . . 10
139134, 135, 133, 136, 138ltletrd 9220 . . . . . . . . 9
14073ad2antrr 707 . . . . . . . . . 10
141 elioopnf 10988 . . . . . . . . . 10
142140, 141syl 16 . . . . . . . . 9
143133, 139, 142mpbir2and 889 . . . . . . . 8
144143, 1syl6eleqr 2526 . . . . . . 7
145130, 144ffvelrnd 5863 . . . . . 6
14697adantr 452 . . . . . . . 8
14798adantr 452 . . . . . . . 8
14816ad2antrr 707 . . . . . . . 8
14969adantr 452 . . . . . . . 8
150100adantlr 696 . . . . . . . 8
151101adantlr 696 . . . . . . . 8
152102adantlr 696 . . . . . . . 8
153103adantr 452 . . . . . . . 8
154104adantr 452 . . . . . . . 8
1551053adant1r 1177 . . . . . . . 8
156 elfzelz 11049 . . . . . . . . . . . 12
157156adantl 453 . . . . . . . . . . 11
158157zred 10365 . . . . . . . . . 10
15971adantr 452 . . . . . . . . . . 11
16080ad2antrr 707 . . . . . . . . . . 11
161 elfzle1 11050 . . . . . . . . . . . 12
162161adantl 453 . . . . . . . . . . 11
163149, 159, 158, 160, 162ltletrd 9220 . . . . . . . . . 10
164149rexrd 9124 . . . . . . . . . . 11
165164, 141syl 16 . . . . . . . . . 10
166158, 163, 165mpbir2and 889 . . . . . . . . 9
167166, 1syl6eleqr 2526 . . . . . . . 8
168 peano2re 9229 . . . . . . . . . . 11
169158, 168syl 16 . . . . . . . . . 10
170158lep1d 9932 . . . . . . . . . . 11
171149, 158, 169, 163, 170ltletrd 9220 . . . . . . . . . 10
172 elioopnf 10988 . . . . . . . . . . 11
173164, 172syl 16 . . . . . . . . . 10
174169, 171, 173mpbir2and 889 . . . . . . . . 9
175174, 1syl6eleqr 2526 . . . . . . . 8
176108adantr 452 . . . . . . . . 9
177147, 159, 158, 176, 162letrd 9217 . . . . . . . 8
178169rexrd 9124 . . . . . . . . 9
17968rexrd 9124 . . . . . . . . . 10
180179adantr 452 . . . . . . . . 9
181 elfzle2 11051 . . . . . . . . . . 11
182181adantl 453 . . . . . . . . . 10
183 1re 9080 . . . . . . . . . . . 12
184183a1i 11 . . . . . . . . . . 11
18566adantr 452 . . . . . . . . . . . 12
186185, 67syl 16 . . . . . . . . . . 11
187 leaddsub 9494 . . . . . . . . . . 11
188158, 184, 186, 187syl3anc 1184 . . . . . . . . . 10
189182, 188mpbird 224 . . . . . . . . 9
19066rexrd 9124 . . . . . . . . . . 11
191179, 190, 104, 111, 112xrletrd 10742 . . . . . . . . . 10
192191adantr 452 . . . . . . . . 9
193178, 180, 154, 189, 192xrletrd 10742 . . . . . . . 8
194 flid 11206 . . . . . . . . . . . 12
195157, 194syl 16 . . . . . . . . . . 11
196195eqcomd 2440 . . . . . . . . . 10
197196oveq1d 6088 . . . . . . . . 9
198 eqle 9166 . . . . . . . . 9
199169, 197, 198syl2anc 643 . . . . . . . 8
2001, 11, 146, 147, 148, 149, 150, 151, 152, 153, 28, 154, 155, 33, 167, 175, 177, 170, 193, 199dvfsumlem2 19901 . . . . . . 7
201200simpld 446 . . . . . 6
202129, 145, 201monoord2 11344 . . . . 5
20371rexrd 9124 . . . . . . . 8
204203, 179, 104, 87, 191xrletrd 10742 . . . . . . 7
20571leidd 9583 . . . . . . 7
2061, 11, 97, 98, 99, 69, 100, 101, 102, 103, 28, 104, 105, 33, 95, 125, 106, 107, 204, 205dvfsumlem2 19901 . . . . . 6
207206simpld 446 . . . . 5
20894, 126, 96, 202, 207letrd 9217 . . . 4
20965, 94, 96, 120, 208letrd 9217 . . 3
21049ralrimiva 2781 . . . . . . . . 9
211210adantr 452 . . . . . . . 8
212 nfcsb1v 3275 . . . . . . . . . 10
213212nfel1 2581 . . . . . . . . 9
214 csbeq1a 3251 . . . . . . . . . 10
215214eleq1d 2501 . . . . . . . . 9
216213, 215rspc 3038 . . . . . . . 8
217211, 216mpan9 456 . . . . . . 7
218217ralrimiva 2781 . . . . . 6
219 csbeq1 3246 . . . . . . . 8
220219eleq1d 2501 . . . . . . 7
221220rspcv 3040 . . . . . 6
22295, 218, 221sylc 58 . . . . 5
22396, 222resubcld 9455 . . . 4
224 csbeq1 3246 . . . . . . . 8
225224eleq1d 2501 . . . . . . 7
226225rspcv 3040 . . . . . 6
22793, 218, 226sylc 58 . . . . 5
22894, 227resubcld 9455 . . . 4
229 csbeq1 3246 . . . . . . . 8
230229eleq1d 2501 . . . . . . 7
231230rspcv 3040 . . . . . 6
23264, 218, 231sylc 58 . . . . 5
23365, 232resubcld 9455 . . . 4
234 csbeq1 3246 . . . . . . . . 9
235234eleq1d 2501 . . . . . . . 8
236235rspcv 3040 . . . . . . 7
237125, 218, 236sylc 58 . . . . . 6
238126, 237resubcld 9455 . . . . 5
239206simprd 450 . . . . 5
240 vex 2951 . . . . . . . . 9
241 fveq2 5720 . . . . . . . . . . 11
242 csbeq1 3246 . . . . . . . . . . 11
243241, 242oveq12d 6091 . . . . . . . . . 10
244 eqid 2435 . . . . . . . . . 10
245 ovex 6098 . . . . . . . . . 10
246243, 244, 245fvmpt3i 5801 . . . . . . . . 9
247240, 246ax-mp 8 . . . . . . . 8
248144, 217syldan 457 . . . . . . . . 9
249145, 248resubcld 9455 . . . . . . . 8
250247, 249syl5eqel 2519 . . . . . . 7
251200simprd 450 . . . . . . . 8
252 ovex 6098 . . . . . . . . 9
253 fveq2 5720 . . . . . . . . . . 11
254 csbeq1 3246 . . . . . . . . . . 11
255253, 254oveq12d 6091 . . . . . . . . . 10
256255, 244, 245fvmpt3i 5801 . . . . . . . . 9
257252, 256ax-mp 8 . . . . . . . 8
258251, 247, 2573brtr4g 4236 . . . . . . 7
259129, 250, 258monoord 11343 . . . . . 6
260 ovex 6098 . . . . . . 7
261 fveq2 5720 . . . . . . . . 9
262 csbeq1 3246 . . . . . . . . 9
263261, 262oveq12d 6091 . . . . . . . 8
264263, 244, 245fvmpt3i 5801 . . . . . . 7
265260, 264ax-mp 8 . . . . . 6
266 fvex 5734 . . . . . . 7
267 fveq2 5720 . . . . . . . . 9
268 csbeq1 3246 . . . . . . . . 9
269267, 268oveq12d 6091 . . . . . . . 8
270269, 244, 245fvmpt3i 5801 . . . . . . 7
271266, 270ax-mp 8 . . . . . 6
272259, 265, 2713brtr3g 4235 . . . . 5
273223, 238, 228, 239, 272letrd 9217 . . . 4
274119simprd 450 . . . 4
275223, 228, 233, 273, 274letrd 9217 . . 3
276209, 275jca 519 . 2
2775, 10, 43, 276lecasei 9169 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2697  cvv 2948  csb 3243   wss 3312   class class class wbr 4204   cmpt 4258  wf 5442  cfv 5446  (class class class)co 6073  cr 8979  c1 8981   caddc 8983   cmul 8985   cpnf 9107  cxr 9109   clt 9110   cle 9111   cmin 9281  cz 10272  cuz 10478  cioo 10906  cfz 11033  cfl 11191  csu 12469   cdv 19740 This theorem is referenced by:  dvfsumlem4  19903  dvfsum2  19908 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7586  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057  ax-pre-sup 9058  ax-addf 9059  ax-mulf 9060 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-ixp 7056  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-fi 7408  df-sup 7438  df-oi 7469  df-card 7816  df-cda 8038  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-div 9668  df-nn 9991  df-2 10048  df-3 10049  df-4 10050  df-5 10051  df-6 10052  df-7 10053  df-8 10054  df-9 10055  df-10 10056  df-n0 10212  df-z 10273  df-dec 10373  df-uz 10479  df-q 10565  df-rp 10603  df-xneg 10700  df-xadd 10701  df-xmul 10702  df-ioo 10910  df-ico 10912  df-icc 10913  df-fz 11034  df-fzo 11126  df-fl 11192  df-seq 11314  df-exp 11373  df-hash 11609  df-cj 11894  df-re 11895  df-im 11896  df-sqr 12030  df-abs 12031  df-clim 12272  df-sum 12470  df-struct 13461  df-ndx 13462  df-slot 13463  df-base 13464  df-sets 13465  df-ress 13466  df-plusg 13532  df-mulr 13533  df-starv 13534  df-sca 13535  df-vsca 13536  df-tset 13538  df-ple 13539  df-ds 13541  df-unif 13542  df-hom 13543  df-cco 13544  df-rest 13640  df-topn 13641  df-topgen 13657  df-pt 13658  df-prds 13661  df-xrs 13716  df-0g 13717  df-gsum 13718  df-qtop 13723  df-imas 13724  df-xps 13726  df-mre 13801  df-mrc 13802  df-acs 13804  df-mnd 14680  df-submnd 14729  df-mulg 14805  df-cntz 15106  df-cmn 15404  df-psmet 16684  df-xmet 16685  df-met 16686  df-bl 16687  df-mopn 16688  df-fbas 16689  df-fg 16690  df-cnfld 16694  df-top 16953  df-bases 16955  df-topon 16956  df-topsp 16957  df-cld 17073  df-ntr 17074  df-cls 17075  df-nei 17152  df-lp 17190  df-perf 17191  df-cn 17281  df-cnp 17282  df-haus 17369  df-cmp 17440  df-tx 17584  df-hmeo 17777  df-fil 17868  df-fm 17960  df-flim 17961  df-flf 17962  df-xms 18340  df-ms 18341  df-tms 18342  df-cncf 18898  df-limc 19743  df-dv 19744
 Copyright terms: Public domain W3C validator