Metamath Proof Explorer

Theorem dvfsumrlim

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 A ( x ) = S. u e. ( M , x ) B ( u ) _d u 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 )
Assertion dvfsumrlim 
|- ( ph -> G e. dom ~~>r )

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 ioossre 
 |-  ( T (,) +oo ) C_ RR
16 1 15 eqsstri 
 |-  S C_ RR
17 16 a1i 
 |-  ( ph -> S C_ RR )
18 1 2 3 4 5 6 7 8 9 10 11 13 dvfsumrlimf 
 |-  ( ph -> G : S --> RR )
19 ax-resscn 
 |-  RR C_ CC
20 fss 
 |-  ( ( G : S --> RR /\ RR C_ CC ) -> G : S --> CC )
21 18 19 20 sylancl 
 |-  ( ph -> G : S --> CC )
22 1 supeq1i 
 |-  sup ( S , RR* , < ) = sup ( ( T (,) +oo ) , RR* , < )
23 ressxr 
 |-  RR C_ RR*
24 23 6 sselid 
 |-  ( ph -> T e. RR* )
25 6 renepnfd 
 |-  ( ph -> T =/= +oo )
26 ioopnfsup 
 |-  ( ( T e. RR* /\ T =/= +oo ) -> sup ( ( T (,) +oo ) , RR* , < ) = +oo )
27 24 25 26 syl2anc 
 |-  ( ph -> sup ( ( T (,) +oo ) , RR* , < ) = +oo )
28 22 27 syl5eq 
 |-  ( ph -> sup ( S , RR* , < ) = +oo )
29 8 14 rlimmptrcl 
 |-  ( ( ph /\ x e. S ) -> B e. CC )
30 29 ralrimiva 
 |-  ( ph -> A. x e. S B e. CC )
31 30 17 rlim0 
 |-  ( ph -> ( ( x e. S |-> B ) ~~>r 0 <-> A. e e. RR+ E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) ) )
32 14 31 mpbid 
 |-  ( ph -> A. e e. RR+ E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) )
33 16 a1i 
 |-  ( ( ph /\ e e. RR+ ) -> S C_ RR )
34 peano2re 
 |-  ( T e. RR -> ( T + 1 ) e. RR )
35 6 34 syl 
 |-  ( ph -> ( T + 1 ) e. RR )
36 35 4 ifcld 
 |-  ( ph -> if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) e. RR )
37 36 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) e. RR )
38 rexico 
 |-  ( ( S C_ RR /\ if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) e. RR ) -> ( E. c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) A. x e. S ( c <_ x -> ( abs ` B ) < e ) <-> E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) ) )
39 33 37 38 syl2anc 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) A. x e. S ( c <_ x -> ( abs ` B ) < e ) <-> E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) ) )
40 elicopnf 
 |-  ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) e. RR -> ( c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) <-> ( c e. RR /\ if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) <_ c ) ) )
41 36 40 syl 
 |-  ( ph -> ( c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) <-> ( c e. RR /\ if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) <_ c ) ) )
42 41 simprbda 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> c e. RR )
43 6 adantr 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> T e. RR )
44 43 34 syl 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( T + 1 ) e. RR )
45 43 ltp1d 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> T < ( T + 1 ) )
46 41 simplbda 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) <_ c )
47 4 adantr 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> D e. RR )
48 maxle 
 |-  ( ( D e. RR /\ ( T + 1 ) e. RR /\ c e. RR ) -> ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) <_ c <-> ( D <_ c /\ ( T + 1 ) <_ c ) ) )
49 47 44 42 48 syl3anc 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) <_ c <-> ( D <_ c /\ ( T + 1 ) <_ c ) ) )
50 46 49 mpbid 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( D <_ c /\ ( T + 1 ) <_ c ) )
51 50 simprd 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( T + 1 ) <_ c )
52 43 44 42 45 51 ltletrd 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> T < c )
53 24 adantr 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> T e. RR* )
54 elioopnf 
 |-  ( T e. RR* -> ( c e. ( T (,) +oo ) <-> ( c e. RR /\ T < c ) ) )
55 53 54 syl 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( c e. ( T (,) +oo ) <-> ( c e. RR /\ T < c ) ) )
56 42 52 55 mpbir2and 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> c e. ( T (,) +oo ) )
57 56 1 eleqtrrdi 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> c e. S )
58 50 simpld 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> D <_ c )
59 57 58 jca 
 |-  ( ( ph /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( c e. S /\ D <_ c ) )
60 59 adantlr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( c e. S /\ D <_ c ) )
61 simprrl 
 |-  ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) -> c e. S )
62 61 adantrr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> c e. S )
63 16 62 sselid 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> c e. RR )
64 63 leidd 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> c <_ c )
65 nfv 
 |-  F/ x c <_ c
66 nfcv 
 |-  F/_ x abs
67 nfcsb1v 
 |-  F/_ x [_ c / x ]_ B
68 66 67 nffv 
 |-  F/_ x ( abs ` [_ c / x ]_ B )
69 nfcv 
 |-  F/_ x <
70 nfcv 
 |-  F/_ x e
71 68 69 70 nfbr 
 |-  F/ x ( abs ` [_ c / x ]_ B ) < e
72 65 71 nfim 
 |-  F/ x ( c <_ c -> ( abs ` [_ c / x ]_ B ) < e )
73 breq2 
 |-  ( x = c -> ( c <_ x <-> c <_ c ) )
74 csbeq1a 
 |-  ( x = c -> B = [_ c / x ]_ B )
75 74 fveq2d 
 |-  ( x = c -> ( abs ` B ) = ( abs ` [_ c / x ]_ B ) )
76 75 breq1d 
 |-  ( x = c -> ( ( abs ` B ) < e <-> ( abs ` [_ c / x ]_ B ) < e ) )
77 73 76 imbi12d 
 |-  ( x = c -> ( ( c <_ x -> ( abs ` B ) < e ) <-> ( c <_ c -> ( abs ` [_ c / x ]_ B ) < e ) ) )
78 72 77 rspc 
 |-  ( c e. S -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c <_ c -> ( abs ` [_ c / x ]_ B ) < e ) ) )
79 62 78 syl 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c <_ c -> ( abs ` [_ c / x ]_ B ) < e ) ) )
80 64 79 mpid 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( abs ` [_ c / x ]_ B ) < e ) )
81 17 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
82 81 adantrr 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> B e. RR )
83 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dvfsumrlimge0 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )
84 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
85 82 83 84 sylanbrc 
 |-  ( ( ph /\ ( x e. S /\ D <_ x ) ) -> B e. ( 0 [,) +oo ) )
86 85 expr 
 |-  ( ( ph /\ x e. S ) -> ( D <_ x -> B e. ( 0 [,) +oo ) ) )
87 86 ralrimiva 
 |-  ( ph -> A. x e. S ( D <_ x -> B e. ( 0 [,) +oo ) ) )
88 87 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> A. x e. S ( D <_ x -> B e. ( 0 [,) +oo ) ) )
89 simprrr 
 |-  ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) -> D <_ c )
90 89 adantrr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> D <_ c )
91 nfv 
 |-  F/ x D <_ c
92 67 nfel1 
 |-  F/ x [_ c / x ]_ B e. ( 0 [,) +oo )
93 91 92 nfim 
 |-  F/ x ( D <_ c -> [_ c / x ]_ B e. ( 0 [,) +oo ) )
94 breq2 
 |-  ( x = c -> ( D <_ x <-> D <_ c ) )
95 74 eleq1d 
 |-  ( x = c -> ( B e. ( 0 [,) +oo ) <-> [_ c / x ]_ B e. ( 0 [,) +oo ) ) )
96 94 95 imbi12d 
 |-  ( x = c -> ( ( D <_ x -> B e. ( 0 [,) +oo ) ) <-> ( D <_ c -> [_ c / x ]_ B e. ( 0 [,) +oo ) ) ) )
97 93 96 rspc 
 |-  ( c e. S -> ( A. x e. S ( D <_ x -> B e. ( 0 [,) +oo ) ) -> ( D <_ c -> [_ c / x ]_ B e. ( 0 [,) +oo ) ) ) )
98 62 88 90 97 syl3c 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> [_ c / x ]_ B e. ( 0 [,) +oo ) )
99 elrege0 
 |-  ( [_ c / x ]_ B e. ( 0 [,) +oo ) <-> ( [_ c / x ]_ B e. RR /\ 0 <_ [_ c / x ]_ B ) )
100 98 99 sylib 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( [_ c / x ]_ B e. RR /\ 0 <_ [_ c / x ]_ B ) )
101 absid 
 |-  ( ( [_ c / x ]_ B e. RR /\ 0 <_ [_ c / x ]_ B ) -> ( abs ` [_ c / x ]_ B ) = [_ c / x ]_ B )
102 100 101 syl 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( abs ` [_ c / x ]_ B ) = [_ c / x ]_ B )
103 102 breq1d 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( ( abs ` [_ c / x ]_ B ) < e <-> [_ c / x ]_ B < e ) )
104 3 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> M e. ZZ )
105 4 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> D e. RR )
106 5 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> M <_ ( D + 1 ) )
107 6 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> T e. RR )
108 7 adantlr 
 |-  ( ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) /\ x e. S ) -> A e. RR )
109 8 adantlr 
 |-  ( ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) /\ x e. S ) -> B e. V )
110 9 adantlr 
 |-  ( ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) /\ x e. Z ) -> B e. RR )
111 10 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
112 pnfxr 
 |-  +oo e. RR*
113 112 a1i 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> +oo e. RR* )
114 3simpa 
 |-  ( ( D <_ x /\ x <_ k /\ k <_ +oo ) -> ( D <_ x /\ x <_ k ) )
115 114 12 syl3an3 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ +oo ) ) -> C <_ B )
116 115 3adant1r 
 |-  ( ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ +oo ) ) -> C <_ B )
117 83 3adantr3 
 |-  ( ( ph /\ ( x e. S /\ D <_ x /\ x <_ +oo ) ) -> 0 <_ B )
118 117 adantlr 
 |-  ( ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) /\ ( x e. S /\ D <_ x /\ x <_ +oo ) ) -> 0 <_ B )
119 simprrl 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> y e. S )
120 simprrr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> c <_ y )
121 16 23 sstri 
 |-  S C_ RR*
122 121 119 sselid 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> y e. RR* )
123 pnfge 
 |-  ( y e. RR* -> y <_ +oo )
124 122 123 syl 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> y <_ +oo )
125 1 2 104 105 106 107 108 109 110 111 11 113 116 13 118 62 119 90 120 124 dvfsumlem4 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) <_ [_ c / x ]_ B )
126 21 adantr 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> G : S --> CC )
127 126 119 ffvelrnd 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( G ` y ) e. CC )
128 126 62 ffvelrnd 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( G ` c ) e. CC )
129 127 128 subcld 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( ( G ` y ) - ( G ` c ) ) e. CC )
130 129 abscld 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) e. RR )
131 100 simpld 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> [_ c / x ]_ B e. RR )
132 simprll 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> e e. RR+ )
133 132 rpred 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> e e. RR )
134 lelttr 
 |-  ( ( ( abs ` ( ( G ` y ) - ( G ` c ) ) ) e. RR /\ [_ c / x ]_ B e. RR /\ e e. RR ) -> ( ( ( abs ` ( ( G ` y ) - ( G ` c ) ) ) <_ [_ c / x ]_ B /\ [_ c / x ]_ B < e ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
135 130 131 133 134 syl3anc 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( ( ( abs ` ( ( G ` y ) - ( G ` c ) ) ) <_ [_ c / x ]_ B /\ [_ c / x ]_ B < e ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
136 125 135 mpand 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( [_ c / x ]_ B < e -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
137 103 136 sylbid 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( ( abs ` [_ c / x ]_ B ) < e -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
138 80 137 syld 
 |-  ( ( ph /\ ( ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) /\ ( y e. S /\ c <_ y ) ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
139 138 anassrs 
 |-  ( ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) /\ ( y e. S /\ c <_ y ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
140 139 expr 
 |-  ( ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) /\ y e. S ) -> ( c <_ y -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
141 140 com23 
 |-  ( ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) /\ y e. S ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
142 141 ralrimdva 
 |-  ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
143 142 61 jctild 
 |-  ( ( ph /\ ( e e. RR+ /\ ( c e. S /\ D <_ c ) ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c e. S /\ A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) ) )
144 143 anassrs 
 |-  ( ( ( ph /\ e e. RR+ ) /\ ( c e. S /\ D <_ c ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c e. S /\ A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) ) )
145 60 144 syldan 
 |-  ( ( ( ph /\ e e. RR+ ) /\ c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) ) -> ( A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> ( c e. S /\ A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) ) )
146 145 expimpd 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) /\ A. x e. S ( c <_ x -> ( abs ` B ) < e ) ) -> ( c e. S /\ A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) ) )
147 146 reximdv2 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. c e. ( if ( D <_ ( T + 1 ) , ( T + 1 ) , D ) [,) +oo ) A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> E. c e. S A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
148 39 147 sylbird 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> E. c e. S A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
149 148 ralimdva 
 |-  ( ph -> ( A. e e. RR+ E. c e. RR A. x e. S ( c <_ x -> ( abs ` B ) < e ) -> A. e e. RR+ E. c e. S A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) ) )
150 32 149 mpd 
 |-  ( ph -> A. e e. RR+ E. c e. S A. y e. S ( c <_ y -> ( abs ` ( ( G ` y ) - ( G ` c ) ) ) < e ) )
151 17 21 28 150 caucvgr 
 |-  ( ph -> G e. dom ~~>r )