Metamath Proof Explorer

Theorem dvfsumabs

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Hypotheses dvfsumabs.m 
|- ( ph -> N e. ( ZZ>= ` M ) )
dvfsumabs.a 
|- ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> CC ) )
dvfsumabs.v 
|- ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )
dvfsumabs.b 
|- ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
dvfsumabs.c 
|- ( x = M -> A = C )
dvfsumabs.d 
|- ( x = N -> A = D )
dvfsumabs.x 
|- ( ( ph /\ k e. ( M ..^ N ) ) -> X e. CC )
dvfsumabs.y 
|- ( ( ph /\ k e. ( M ..^ N ) ) -> Y e. RR )
dvfsumabs.l 
|- ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> ( abs ` ( X - B ) ) <_ Y )
Assertion dvfsumabs 
|- ( ph -> ( abs ` ( sum_ k e. ( M ..^ N ) X - ( D - C ) ) ) <_ sum_ k e. ( M ..^ N ) Y )

Proof

Step Hyp Ref Expression
1 dvfsumabs.m 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 dvfsumabs.a 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> CC ) )
3 dvfsumabs.v 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )
4 dvfsumabs.b 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
5 dvfsumabs.c 
 |-  ( x = M -> A = C )
6 dvfsumabs.d 
 |-  ( x = N -> A = D )
7 dvfsumabs.x 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. CC )
8 dvfsumabs.y 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> Y e. RR )
9 dvfsumabs.l 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> ( abs ` ( X - B ) ) <_ Y )
10 fzofi 
 |-  ( M ..^ N ) e. Fin
11 10 a1i 
 |-  ( ph -> ( M ..^ N ) e. Fin )
12 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
13 1 12 syl 
 |-  ( ph -> M e. ZZ )
14 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
15 1 14 syl 
 |-  ( ph -> N e. ZZ )
16 fzval2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )
17 13 15 16 syl2anc 
 |-  ( ph -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )
18 inss1 
 |-  ( ( M [,] N ) i^i ZZ ) C_ ( M [,] N )
19 17 18 eqsstrdi 
 |-  ( ph -> ( M ... N ) C_ ( M [,] N ) )
20 19 sselda 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> y e. ( M [,] N ) )
21 cncff 
 |-  ( ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> CC ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> CC )
22 2 21 syl 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> CC )
23 eqid 
 |-  ( x e. ( M [,] N ) |-> A ) = ( x e. ( M [,] N ) |-> A )
24 23 fmpt 
 |-  ( A. x e. ( M [,] N ) A e. CC <-> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> CC )
25 22 24 sylibr 
 |-  ( ph -> A. x e. ( M [,] N ) A e. CC )
26 nfcsb1v 
 |-  F/_ x [_ y / x ]_ A
27 26 nfel1 
 |-  F/ x [_ y / x ]_ A e. CC
28 csbeq1a 
 |-  ( x = y -> A = [_ y / x ]_ A )
29 28 eleq1d 
 |-  ( x = y -> ( A e. CC <-> [_ y / x ]_ A e. CC ) )
30 27 29 rspc 
 |-  ( y e. ( M [,] N ) -> ( A. x e. ( M [,] N ) A e. CC -> [_ y / x ]_ A e. CC ) )
31 25 30 mpan9 
 |-  ( ( ph /\ y e. ( M [,] N ) ) -> [_ y / x ]_ A e. CC )
32 20 31 syldan 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> [_ y / x ]_ A e. CC )
33 32 ralrimiva 
 |-  ( ph -> A. y e. ( M ... N ) [_ y / x ]_ A e. CC )
34 fzofzp1 
 |-  ( k e. ( M ..^ N ) -> ( k + 1 ) e. ( M ... N ) )
35 csbeq1 
 |-  ( y = ( k + 1 ) -> [_ y / x ]_ A = [_ ( k + 1 ) / x ]_ A )
36 35 eleq1d 
 |-  ( y = ( k + 1 ) -> ( [_ y / x ]_ A e. CC <-> [_ ( k + 1 ) / x ]_ A e. CC ) )
37 36 rspccva 
 |-  ( ( A. y e. ( M ... N ) [_ y / x ]_ A e. CC /\ ( k + 1 ) e. ( M ... N ) ) -> [_ ( k + 1 ) / x ]_ A e. CC )
38 33 34 37 syl2an 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> [_ ( k + 1 ) / x ]_ A e. CC )
39 elfzofz 
 |-  ( k e. ( M ..^ N ) -> k e. ( M ... N ) )
40 csbeq1 
 |-  ( y = k -> [_ y / x ]_ A = [_ k / x ]_ A )
41 40 eleq1d 
 |-  ( y = k -> ( [_ y / x ]_ A e. CC <-> [_ k / x ]_ A e. CC ) )
42 41 rspccva 
 |-  ( ( A. y e. ( M ... N ) [_ y / x ]_ A e. CC /\ k e. ( M ... N ) ) -> [_ k / x ]_ A e. CC )
43 33 39 42 syl2an 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> [_ k / x ]_ A e. CC )
44 38 43 subcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) e. CC )
45 11 7 44 fsumsub 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( sum_ k e. ( M ..^ N ) X - sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) )
46 vex 
 |-  y e. _V
47 46 a1i 
 |-  ( y = M -> y e. _V )
48 eqeq2 
 |-  ( y = M -> ( x = y <-> x = M ) )
49 48 biimpa 
 |-  ( ( y = M /\ x = y ) -> x = M )
50 49 5 syl 
 |-  ( ( y = M /\ x = y ) -> A = C )
51 47 50 csbied 
 |-  ( y = M -> [_ y / x ]_ A = C )
52 46 a1i 
 |-  ( y = N -> y e. _V )
53 eqeq2 
 |-  ( y = N -> ( x = y <-> x = N ) )
54 53 biimpa 
 |-  ( ( y = N /\ x = y ) -> x = N )
55 54 6 syl 
 |-  ( ( y = N /\ x = y ) -> A = D )
56 52 55 csbied 
 |-  ( y = N -> [_ y / x ]_ A = D )
57 40 35 51 56 1 32 telfsumo2 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) = ( D - C ) )
58 57 oveq2d 
 |-  ( ph -> ( sum_ k e. ( M ..^ N ) X - sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( sum_ k e. ( M ..^ N ) X - ( D - C ) ) )
59 45 58 eqtrd 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( sum_ k e. ( M ..^ N ) X - ( D - C ) ) )
60 59 fveq2d 
 |-  ( ph -> ( abs ` sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) = ( abs ` ( sum_ k e. ( M ..^ N ) X - ( D - C ) ) ) )
61 7 44 subcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) e. CC )
62 11 61 fsumcl 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) e. CC )
63 62 abscld 
 |-  ( ph -> ( abs ` sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) e. RR )
64 61 abscld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) e. RR )
65 11 64 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) e. RR )
66 11 8 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ..^ N ) Y e. RR )
67 11 61 fsumabs 
 |-  ( ph -> ( abs ` sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) <_ sum_ k e. ( M ..^ N ) ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) )
68 elfzoelz 
 |-  ( k e. ( M ..^ N ) -> k e. ZZ )
69 68 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. ZZ )
70 69 zred 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. RR )
71 70 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. RR* )
72 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
73 70 72 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. RR )
74 73 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. RR* )
75 70 lep1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k <_ ( k + 1 ) )
76 ubicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
77 71 74 75 76 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
78 lbicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> k e. ( k [,] ( k + 1 ) ) )
79 71 74 75 78 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. ( k [,] ( k + 1 ) ) )
80 13 zred 
 |-  ( ph -> M e. RR )
81 80 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR )
82 15 zred 
 |-  ( ph -> N e. RR )
83 82 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR )
84 elfzole1 
 |-  ( k e. ( M ..^ N ) -> M <_ k )
85 84 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M <_ k )
86 34 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
87 elfzle2 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( k + 1 ) <_ N )
88 86 87 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) <_ N )
89 iccss 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ ( M <_ k /\ ( k + 1 ) <_ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
90 81 83 85 88 89 syl22anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
91 90 resmptd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> ( ( X x. x ) - A ) ) |` ( k [,] ( k + 1 ) ) ) = ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) )
92 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
93 92 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
94 93 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
95 iccssre 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M [,] N ) C_ RR )
96 80 82 95 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ RR )
97 96 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ RR )
98 ax-resscn 
 |-  RR C_ CC
99 97 98 sstrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ CC )
100 ssid 
 |-  CC C_ CC
101 100 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> CC C_ CC )
102 cncfmptc 
 |-  ( ( X e. CC /\ ( M [,] N ) C_ CC /\ CC C_ CC ) -> ( x e. ( M [,] N ) |-> X ) e. ( ( M [,] N ) -cn-> CC ) )
103 7 99 101 102 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> X ) e. ( ( M [,] N ) -cn-> CC ) )
104 cncfmptid 
 |-  ( ( ( M [,] N ) C_ CC /\ CC C_ CC ) -> ( x e. ( M [,] N ) |-> x ) e. ( ( M [,] N ) -cn-> CC ) )
105 99 100 104 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> x ) e. ( ( M [,] N ) -cn-> CC ) )
106 103 105 mulcncf 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> ( X x. x ) ) e. ( ( M [,] N ) -cn-> CC ) )
107 2 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> CC ) )
108 92 94 106 107 cncfmpt2f 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> ( ( X x. x ) - A ) ) e. ( ( M [,] N ) -cn-> CC ) )
109 rescncf 
 |-  ( ( k [,] ( k + 1 ) ) C_ ( M [,] N ) -> ( ( x e. ( M [,] N ) |-> ( ( X x. x ) - A ) ) e. ( ( M [,] N ) -cn-> CC ) -> ( ( x e. ( M [,] N ) |-> ( ( X x. x ) - A ) ) |` ( k [,] ( k + 1 ) ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> CC ) ) )
110 90 108 109 sylc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> ( ( X x. x ) - A ) ) |` ( k [,] ( k + 1 ) ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> CC ) )
111 91 110 eqeltrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> CC ) )
112 98 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR C_ CC )
113 90 97 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ RR )
114 90 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k [,] ( k + 1 ) ) ) -> x e. ( M [,] N ) )
115 7 adantr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> X e. CC )
116 99 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> x e. CC )
117 115 116 mulcld 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> ( X x. x ) e. CC )
118 25 r19.21bi 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. CC )
119 118 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> A e. CC )
120 117 119 subcld 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> ( ( X x. x ) - A ) e. CC )
121 114 120 syldan 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k [,] ( k + 1 ) ) ) -> ( ( X x. x ) - A ) e. CC )
122 92 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
123 iccntr 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( k [,] ( k + 1 ) ) ) = ( k (,) ( k + 1 ) ) )
124 70 73 123 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( k [,] ( k + 1 ) ) ) = ( k (,) ( k + 1 ) ) )
125 112 113 121 122 92 124 dvmptntr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = ( RR _D ( x e. ( k (,) ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) )
126 reelprrecn 
 |-  RR e. { RR , CC }
127 126 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR e. { RR , CC } )
128 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
129 128 sseli 
 |-  ( x e. ( M (,) N ) -> x e. ( M [,] N ) )
130 129 120 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> ( ( X x. x ) - A ) e. CC )
131 ovex 
 |-  ( X - B ) e. _V
132 131 a1i 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> ( X - B ) e. _V )
133 129 117 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> ( X x. x ) e. CC )
134 7 adantr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> X e. CC )
135 128 99 sstrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) N ) C_ CC )
136 135 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> x e. CC )
137 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> 1 e. CC )
138 112 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. RR ) -> x e. CC )
139 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. RR ) -> 1 e. CC )
140 127 dvmptid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
141 128 97 sstrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) N ) C_ RR )
142 iooretop 
 |-  ( M (,) N ) e. ( topGen ` ran (,) )
143 142 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) N ) e. ( topGen ` ran (,) ) )
144 127 138 139 140 141 122 92 143 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> x ) ) = ( x e. ( M (,) N ) |-> 1 ) )
145 127 136 137 144 7 dvmptcmul 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> ( X x. x ) ) ) = ( x e. ( M (,) N ) |-> ( X x. 1 ) ) )
146 7 mulid1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. 1 ) = X )
147 146 mpteq2dv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> ( X x. 1 ) ) = ( x e. ( M (,) N ) |-> X ) )
148 145 147 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> ( X x. x ) ) ) = ( x e. ( M (,) N ) |-> X ) )
149 129 119 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> A e. CC )
150 3 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> B e. V )
151 4 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
152 127 133 134 148 149 150 151 dvmptsub 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> ( ( X x. x ) - A ) ) ) = ( x e. ( M (,) N ) |-> ( X - B ) ) )
153 81 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR* )
154 iooss1 
 |-  ( ( M e. RR* /\ M <_ k ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
155 153 85 154 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
156 83 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR* )
157 iooss2 
 |-  ( ( N e. RR* /\ ( k + 1 ) <_ N ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
158 156 88 157 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
159 155 158 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) N ) )
160 iooretop 
 |-  ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) )
161 160 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) ) )
162 127 130 132 152 159 122 92 161 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( k (,) ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) )
163 125 162 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) )
164 163 dmeqd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = dom ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) )
165 eqid 
 |-  ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) = ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) )
166 131 165 dmmpti 
 |-  dom ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) = ( k (,) ( k + 1 ) )
167 164 166 eqtrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = ( k (,) ( k + 1 ) ) )
168 163 adantr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) = ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) )
169 168 fveq1d 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) = ( ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) ` x ) )
170 simpr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> x e. ( k (,) ( k + 1 ) ) )
171 165 fvmpt2 
 |-  ( ( x e. ( k (,) ( k + 1 ) ) /\ ( X - B ) e. _V ) -> ( ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) ` x ) = ( X - B ) )
172 170 131 171 sylancl 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( ( x e. ( k (,) ( k + 1 ) ) |-> ( X - B ) ) ` x ) = ( X - B ) )
173 169 172 eqtrd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) = ( X - B ) )
174 173 fveq2d 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) = ( abs ` ( X - B ) ) )
175 9 anassrs 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( abs ` ( X - B ) ) <_ Y )
176 174 175 eqbrtrd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) <_ Y )
177 176 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( k (,) ( k + 1 ) ) ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) <_ Y )
178 nfcv 
 |-  F/_ x abs
179 nfcv 
 |-  F/_ x RR
180 nfcv 
 |-  F/_ x _D
181 nfmpt1 
 |-  F/_ x ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) )
182 179 180 181 nfov 
 |-  F/_ x ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) )
183 nfcv 
 |-  F/_ x y
184 182 183 nffv 
 |-  F/_ x ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y )
185 178 184 nffv 
 |-  F/_ x ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) )
186 nfcv 
 |-  F/_ x <_
187 nfcv 
 |-  F/_ x Y
188 185 186 187 nfbr 
 |-  F/ x ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) ) <_ Y
189 2fveq3 
 |-  ( x = y -> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) = ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) ) )
190 189 breq1d 
 |-  ( x = y -> ( ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) <_ Y <-> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) ) <_ Y ) )
191 188 190 rspc 
 |-  ( y e. ( k (,) ( k + 1 ) ) -> ( A. x e. ( k (,) ( k + 1 ) ) ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` x ) ) <_ Y -> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) ) <_ Y ) )
192 177 191 mpan9 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> ( abs ` ( ( RR _D ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ) ` y ) ) <_ Y )
193 70 73 111 167 8 192 dvlip 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ ( ( k + 1 ) e. ( k [,] ( k + 1 ) ) /\ k e. ( k [,] ( k + 1 ) ) ) ) -> ( abs ` ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) ) <_ ( Y x. ( abs ` ( ( k + 1 ) - k ) ) ) )
194 193 ex 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( ( k + 1 ) e. ( k [,] ( k + 1 ) ) /\ k e. ( k [,] ( k + 1 ) ) ) -> ( abs ` ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) ) <_ ( Y x. ( abs ` ( ( k + 1 ) - k ) ) ) ) )
195 77 79 194 mp2and 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) ) <_ ( Y x. ( abs ` ( ( k + 1 ) - k ) ) ) )
196 ovex 
 |-  ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) e. _V
197 nfcv 
 |-  F/_ x ( k + 1 )
198 nfcv 
 |-  F/_ x ( X x. ( k + 1 ) )
199 nfcv 
 |-  F/_ x -
200 nfcsb1v 
 |-  F/_ x [_ ( k + 1 ) / x ]_ A
201 198 199 200 nfov 
 |-  F/_ x ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A )
202 oveq2 
 |-  ( x = ( k + 1 ) -> ( X x. x ) = ( X x. ( k + 1 ) ) )
203 csbeq1a 
 |-  ( x = ( k + 1 ) -> A = [_ ( k + 1 ) / x ]_ A )
204 202 203 oveq12d 
 |-  ( x = ( k + 1 ) -> ( ( X x. x ) - A ) = ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) )
205 eqid 
 |-  ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) = ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) )
206 197 201 204 205 fvmptf 
 |-  ( ( ( k + 1 ) e. ( k [,] ( k + 1 ) ) /\ ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) e. _V ) -> ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) = ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) )
207 77 196 206 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) = ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) )
208 70 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. CC )
209 7 208 mulcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. k ) e. CC )
210 209 43 subcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( X x. k ) - [_ k / x ]_ A ) e. CC )
211 nfcv 
 |-  F/_ x k
212 nfcv 
 |-  F/_ x ( X x. k )
213 nfcsb1v 
 |-  F/_ x [_ k / x ]_ A
214 212 199 213 nfov 
 |-  F/_ x ( ( X x. k ) - [_ k / x ]_ A )
215 oveq2 
 |-  ( x = k -> ( X x. x ) = ( X x. k ) )
216 csbeq1a 
 |-  ( x = k -> A = [_ k / x ]_ A )
217 215 216 oveq12d 
 |-  ( x = k -> ( ( X x. x ) - A ) = ( ( X x. k ) - [_ k / x ]_ A ) )
218 211 214 217 205 fvmptf 
 |-  ( ( k e. ( k [,] ( k + 1 ) ) /\ ( ( X x. k ) - [_ k / x ]_ A ) e. CC ) -> ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) = ( ( X x. k ) - [_ k / x ]_ A ) )
219 79 210 218 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) = ( ( X x. k ) - [_ k / x ]_ A ) )
220 207 219 oveq12d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) = ( ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) - ( ( X x. k ) - [_ k / x ]_ A ) ) )
221 peano2cn 
 |-  ( k e. CC -> ( k + 1 ) e. CC )
222 208 221 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. CC )
223 7 222 mulcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. ( k + 1 ) ) e. CC )
224 223 209 38 43 sub4d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( ( X x. ( k + 1 ) ) - ( X x. k ) ) - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( ( ( X x. ( k + 1 ) ) - [_ ( k + 1 ) / x ]_ A ) - ( ( X x. k ) - [_ k / x ]_ A ) ) )
225 1cnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> 1 e. CC )
226 208 225 pncan2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( k + 1 ) - k ) = 1 )
227 226 oveq2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. ( ( k + 1 ) - k ) ) = ( X x. 1 ) )
228 7 222 208 subdid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. ( ( k + 1 ) - k ) ) = ( ( X x. ( k + 1 ) ) - ( X x. k ) ) )
229 227 228 146 3eqtr3d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( X x. ( k + 1 ) ) - ( X x. k ) ) = X )
230 229 oveq1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( ( X x. ( k + 1 ) ) - ( X x. k ) ) - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) )
231 220 224 230 3eqtr2rd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) = ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) )
232 231 fveq2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) = ( abs ` ( ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` ( k + 1 ) ) - ( ( x e. ( k [,] ( k + 1 ) ) |-> ( ( X x. x ) - A ) ) ` k ) ) ) )
233 226 fveq2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( ( k + 1 ) - k ) ) = ( abs ` 1 ) )
234 abs1 
 |-  ( abs ` 1 ) = 1
235 233 234 eqtrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( ( k + 1 ) - k ) ) = 1 )
236 235 oveq2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( Y x. ( abs ` ( ( k + 1 ) - k ) ) ) = ( Y x. 1 ) )
237 8 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> Y e. CC )
238 237 mulid1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( Y x. 1 ) = Y )
239 236 238 eqtr2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> Y = ( Y x. ( abs ` ( ( k + 1 ) - k ) ) ) )
240 195 232 239 3brtr4d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) <_ Y )
241 11 64 8 240 fsumle 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( abs ` ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) <_ sum_ k e. ( M ..^ N ) Y )
242 63 65 66 67 241 letrd 
 |-  ( ph -> ( abs ` sum_ k e. ( M ..^ N ) ( X - ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) ) ) <_ sum_ k e. ( M ..^ N ) Y )
243 60 242 eqbrtrrd 
 |-  ( ph -> ( abs ` ( sum_ k e. ( M ..^ N ) X - ( D - C ) ) ) <_ sum_ k e. ( M ..^ N ) Y )