Metamath Proof Explorer


Theorem dvfsumrlim2

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 x e. S |-> B is a decreasing function with antiderivative A converging to zero, then the difference between sum_ k e. ( M ... ( |_x ) ) B ( k ) and S. u e. ( M , x ) B ( u ) _d u = A ( x ) converges to a constant limit value, with the remainder term bounded by B ( x ) . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s S = T +∞
dvfsum.z Z = M
dvfsum.m φ M
dvfsum.d φ D
dvfsum.md φ M D + 1
dvfsum.t φ T
dvfsum.a φ x S A
dvfsum.b1 φ x S B V
dvfsum.b2 φ x Z B
dvfsum.b3 φ dx S A d x = x S B
dvfsum.c x = k B = C
dvfsumrlim.l φ x S k S D x x k C B
dvfsumrlim.g G = x S k = M x C A
dvfsumrlim.k φ x S B 0
dvfsumrlim2.1 φ X S
dvfsumrlim2.2 φ D X
Assertion dvfsumrlim2 φ G L G X L X / x B

Proof

Step Hyp Ref Expression
1 dvfsum.s S = T +∞
2 dvfsum.z Z = M
3 dvfsum.m φ M
4 dvfsum.d φ D
5 dvfsum.md φ M D + 1
6 dvfsum.t φ T
7 dvfsum.a φ x S A
8 dvfsum.b1 φ x S B V
9 dvfsum.b2 φ x Z B
10 dvfsum.b3 φ dx S A d x = x S B
11 dvfsum.c x = k B = C
12 dvfsumrlim.l φ x S k S D x x k C B
13 dvfsumrlim.g G = x S k = M x C A
14 dvfsumrlim.k φ x S B 0
15 dvfsumrlim2.1 φ X S
16 dvfsumrlim2.2 φ D X
17 ioossre T +∞
18 1 17 eqsstri S
19 18 15 sseldi φ X
20 19 rexrd φ X *
21 19 renepnfd φ X +∞
22 icopnfsup X * X +∞ sup X +∞ * < = +∞
23 20 21 22 syl2anc φ sup X +∞ * < = +∞
24 23 adantr φ G L sup X +∞ * < = +∞
25 1 2 3 4 5 6 7 8 9 10 11 13 dvfsumrlimf φ G : S
26 25 ad2antrr φ G L y X +∞ G : S
27 15 ad2antrr φ G L y X +∞ X S
28 26 27 ffvelrnd φ G L y X +∞ G X
29 28 recnd φ G L y X +∞ G X
30 6 rexrd φ T *
31 15 1 eleqtrdi φ X T +∞
32 elioopnf T * X T +∞ X T < X
33 30 32 syl φ X T +∞ X T < X
34 31 33 mpbid φ X T < X
35 34 simprd φ T < X
36 df-ioo . = u * , v * w * | u < w w < v
37 df-ico . = u * , v * w * | u w w < v
38 xrltletr T * X * z * T < X X z T < z
39 36 37 38 ixxss1 T * T < X X +∞ T +∞
40 30 35 39 syl2anc φ X +∞ T +∞
41 40 1 sseqtrrdi φ X +∞ S
42 41 adantr φ G L X +∞ S
43 42 sselda φ G L y X +∞ y S
44 26 43 ffvelrnd φ G L y X +∞ G y
45 44 recnd φ G L y X +∞ G y
46 29 45 subcld φ G L y X +∞ G X G y
47 pnfxr +∞ *
48 icossre X +∞ * X +∞
49 19 47 48 sylancl φ X +∞
50 49 adantr φ G L X +∞
51 rlimf G L G : dom G
52 51 adantl φ G L G : dom G
53 ovex k = M x C A V
54 53 13 dmmpti dom G = S
55 54 feq2i G : dom G G : S
56 52 55 sylib φ G L G : S
57 15 adantr φ G L X S
58 56 57 ffvelrnd φ G L G X
59 rlimconst X +∞ G X y X +∞ G X G X
60 50 58 59 syl2anc φ G L y X +∞ G X G X
61 56 feqmptd φ G L G = y S G y
62 simpr φ G L G L
63 61 62 eqbrtrrd φ G L y S G y L
64 42 63 rlimres2 φ G L y X +∞ G y L
65 29 45 60 64 rlimsub φ G L y X +∞ G X G y G X L
66 46 65 rlimabs φ G L y X +∞ G X G y G X L
67 18 a1i φ S
68 67 7 8 10 dvmptrecl φ x S B
69 68 ralrimiva φ x S B
70 nfcsb1v _ x X / x B
71 70 nfel1 x X / x B
72 csbeq1a x = X B = X / x B
73 72 eleq1d x = X B X / x B
74 71 73 rspc X S x S B X / x B
75 15 69 74 sylc φ X / x B
76 75 recnd φ X / x B
77 rlimconst X +∞ X / x B y X +∞ X / x B X / x B
78 49 76 77 syl2anc φ y X +∞ X / x B X / x B
79 78 adantr φ G L y X +∞ X / x B X / x B
80 46 abscld φ G L y X +∞ G X G y
81 75 ad2antrr φ G L y X +∞ X / x B
82 29 45 abssubd φ G L y X +∞ G X G y = G y G X
83 3 adantr φ y X +∞ M
84 4 adantr φ y X +∞ D
85 5 adantr φ y X +∞ M D + 1
86 6 adantr φ y X +∞ T
87 7 adantlr φ y X +∞ x S A
88 8 adantlr φ y X +∞ x S B V
89 9 adantlr φ y X +∞ x Z B
90 10 adantr φ y X +∞ dx S A d x = x S B
91 47 a1i φ y X +∞ +∞ *
92 3simpa D x x k k +∞ D x x k
93 92 12 syl3an3 φ x S k S D x x k k +∞ C B
94 93 3adant1r φ y X +∞ x S k S D x x k k +∞ C B
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dvfsumrlimge0 φ x S D x 0 B
96 95 3adantr3 φ x S D x x +∞ 0 B
97 96 adantlr φ y X +∞ x S D x x +∞ 0 B
98 15 adantr φ y X +∞ X S
99 41 sselda φ y X +∞ y S
100 16 adantr φ y X +∞ D X
101 elicopnf X y X +∞ y X y
102 19 101 syl φ y X +∞ y X y
103 102 simplbda φ y X +∞ X y
104 102 simprbda φ y X +∞ y
105 104 rexrd φ y X +∞ y *
106 pnfge y * y +∞
107 105 106 syl φ y X +∞ y +∞
108 1 2 83 84 85 86 87 88 89 90 11 91 94 13 97 98 99 100 103 107 dvfsumlem4 φ y X +∞ G y G X X / x B
109 108 adantlr φ G L y X +∞ G y G X X / x B
110 82 109 eqbrtrd φ G L y X +∞ G X G y X / x B
111 24 66 79 80 81 110 rlimle φ G L G X L X / x B