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

Theorem dvfsumrlim2 19379
 Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if is a decreasing function with antiderivative converging to zero, then the difference between and converges to a constant limit value, with the remainder term bounded by . (Contributed by Mario Carneiro, 18-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
dvfsumrlim.l
dvfsumrlim.g
dvfsumrlim.k
dvfsumrlim2.1
dvfsumrlim2.2
Assertion
Ref Expression
dvfsumrlim2
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,   ,   ,,
Allowed substitution hints:   (,)   ()   ()   ()   (,)   (,)   (,)   ()

Proof of Theorem dvfsumrlim2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . 7
2 ioossre 10712 . . . . . . 7
31, 2eqsstri 3208 . . . . . 6
4 dvfsumrlim2.1 . . . . . 6
53, 4sseldi 3178 . . . . 5
65rexrd 8881 . . . 4
75renepnfd 8882 . . . 4
8 icopnfsup 10969 . . . 4
96, 7, 8syl2anc 642 . . 3
11 dvfsum.z . . . . . . . 8
12 dvfsum.m . . . . . . . 8
13 dvfsum.d . . . . . . . 8
14 dvfsum.md . . . . . . . 8
15 dvfsum.t . . . . . . . 8
16 dvfsum.a . . . . . . . 8
17 dvfsum.b1 . . . . . . . 8
18 dvfsum.b2 . . . . . . . 8
19 dvfsum.b3 . . . . . . . 8
20 dvfsum.c . . . . . . . 8
21 dvfsumrlim.g . . . . . . . 8
221, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21dvfsumrlimf 19372 . . . . . . 7
2322ad2antrr 706 . . . . . 6
244ad2antrr 706 . . . . . 6
25 ffvelrn 5663 . . . . . 6
2623, 24, 25syl2anc 642 . . . . 5
2726recnd 8861 . . . 4
2815rexrd 8881 . . . . . . . . . 10
294, 1syl6eleq 2373 . . . . . . . . . . . 12
30 elioopnf 10737 . . . . . . . . . . . . 13
3128, 30syl 15 . . . . . . . . . . . 12
3229, 31mpbid 201 . . . . . . . . . . 11
3332simprd 449 . . . . . . . . . 10
34 df-ioo 10660 . . . . . . . . . . 11
35 df-ico 10662 . . . . . . . . . . 11
36 xrltletr 10488 . . . . . . . . . . 11
3734, 35, 36ixxss1 10674 . . . . . . . . . 10
3828, 33, 37syl2anc 642 . . . . . . . . 9
3938, 1syl6sseqr 3225 . . . . . . . 8
4039adantr 451 . . . . . . 7
4140sselda 3180 . . . . . 6
42 ffvelrn 5663 . . . . . 6
4323, 41, 42syl2anc 642 . . . . 5
4443recnd 8861 . . . 4
4527, 44subcld 9157 . . 3
46 pnfxr 10455 . . . . . . 7
47 icossre 10730 . . . . . . 7
485, 46, 47sylancl 643 . . . . . 6
4948adantr 451 . . . . 5
50 rlimf 11975 . . . . . . . 8
5150adantl 452 . . . . . . 7
52 ovex 5883 . . . . . . . . 9
5352, 21dmmpti 5373 . . . . . . . 8
5453feq2i 5384 . . . . . . 7
5551, 54sylib 188 . . . . . 6
564adantr 451 . . . . . 6
57 ffvelrn 5663 . . . . . 6
5855, 56, 57syl2anc 642 . . . . 5
59 rlimconst 12018 . . . . 5
6049, 58, 59syl2anc 642 . . . 4
6155feqmptd 5575 . . . . . 6
62 simpr 447 . . . . . 6
6361, 62eqbrtrrd 4045 . . . . 5
6440, 63rlimres2 12035 . . . 4
6527, 44, 60, 64rlimsub 12117 . . 3
6645, 65rlimabs 12082 . 2
673a1i 10 . . . . . . . 8
6867, 16, 17, 19dvmptrecl 19371 . . . . . . 7
6968ralrimiva 2626 . . . . . 6
70 nfcsb1v 3113 . . . . . . . 8
7170nfel1 2429 . . . . . . 7
72 csbeq1a 3089 . . . . . . . 8
7372eleq1d 2349 . . . . . . 7
7471, 73rspc 2878 . . . . . 6
754, 69, 74sylc 56 . . . . 5
7675recnd 8861 . . . 4
77 rlimconst 12018 . . . 4
7848, 76, 77syl2anc 642 . . 3
8045abscld 11918 . 2
8227, 44abssubd 11935 . . 3
8312adantr 451 . . . . 5
8413adantr 451 . . . . 5
8514adantr 451 . . . . 5
8615adantr 451 . . . . 5
8716adantlr 695 . . . . 5
8817adantlr 695 . . . . 5
8918adantlr 695 . . . . 5
9019adantr 451 . . . . 5
9146a1i 10 . . . . 5
92 3simpa 952 . . . . . . 7
93 dvfsumrlim.l . . . . . . 7
9492, 93syl3an3 1217 . . . . . 6
95943adant1r 1175 . . . . 5
96 dvfsumrlim.k . . . . . . . 8
971, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 93, 21, 96dvfsumrlimge0 19377 . . . . . . 7
98973adantr3 1116 . . . . . 6
9998adantlr 695 . . . . 5
1004adantr 451 . . . . 5
10139sselda 3180 . . . . 5
102 dvfsumrlim2.2 . . . . . 6
103102adantr 451 . . . . 5
104 elicopnf 10739 . . . . . . 7
1055, 104syl 15 . . . . . 6
106105simplbda 607 . . . . 5
107105simprbda 606 . . . . . . 7
108107rexrd 8881 . . . . . 6
109 pnfge 10469 . . . . . 6
110108, 109syl 15 . . . . 5
1111, 11, 83, 84, 85, 86, 87, 88, 89, 90, 20, 91, 95, 21, 99, 100, 101, 103, 106, 110dvfsumlem4 19376 . . . 4