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 (,) +oo )
dvfsum.z 
|- Z = ( ZZ>= ` M )
dvfsum.m 
|- ( ph -> M e. ZZ )
dvfsum.d 
|- ( ph -> D e. RR )
dvfsum.md 
|- ( ph -> M <_ ( D + 1 ) )
dvfsum.t 
|- ( ph -> T e. RR )
dvfsum.a 
|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum.b1 
|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum.b2 
|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum.b3 
|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum.c 
|- ( x = k -> B = C )
dvfsumrlim.l 
|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k ) ) -> C <_ B )
dvfsumrlim.g 
|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
dvfsumrlim.k 
|- ( ph -> ( x e. S |-> B ) ~~>r 0 )
dvfsumrlim2.1 
|- ( ph -> X e. S )
dvfsumrlim2.2 
|- ( ph -> D <_ X )
Assertion dvfsumrlim2 
|- ( ( ph /\ G ~~>r L ) -> ( abs ` ( ( G ` X ) - L ) ) <_ [_ X / x ]_ B )

Proof

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