Metamath Proof Explorer

Theorem gg-dvfsumle

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) Use mpomulcn instead of mulcn as direct dependency. (Revised by GG, 16-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 gg-dvfsumle.m 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 gg-dvfsumle.a 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
3 gg-dvfsumle.v 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )
4 gg-dvfsumle.b 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
5 gg-dvfsumle.c 
 |-  ( x = M -> A = C )
6 gg-dvfsumle.d 
 |-  ( x = N -> A = D )
7 gg-dvfsumle.x 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. RR )
8 gg-dvfsumle.l 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> X <_ B )
9 fzofi 
 |-  ( M ..^ N ) e. Fin
10 9 a1i 
 |-  ( ph -> ( M ..^ N ) e. Fin )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 1 11 syl 
 |-  ( ph -> M e. ZZ )
13 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
14 1 13 syl 
 |-  ( ph -> N e. ZZ )
15 fzval2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )
16 12 14 15 syl2anc 
 |-  ( ph -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )
17 inss1 
 |-  ( ( M [,] N ) i^i ZZ ) C_ ( M [,] N )
18 16 17 eqsstrdi 
 |-  ( ph -> ( M ... N ) C_ ( M [,] N ) )
19 18 sselda 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> y e. ( M [,] N ) )
20 cncff 
 |-  ( ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
21 2 20 syl 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
22 eqid 
 |-  ( x e. ( M [,] N ) |-> A ) = ( x e. ( M [,] N ) |-> A )
23 22 fmpt 
 |-  ( A. x e. ( M [,] N ) A e. RR <-> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
24 21 23 sylibr 
 |-  ( ph -> A. x e. ( M [,] N ) A e. RR )
25 nfcsb1v 
 |-  F/_ x [_ y / x ]_ A
26 25 nfel1 
 |-  F/ x [_ y / x ]_ A e. RR
27 csbeq1a 
 |-  ( x = y -> A = [_ y / x ]_ A )
28 27 eleq1d 
 |-  ( x = y -> ( A e. RR <-> [_ y / x ]_ A e. RR ) )
29 26 28 rspc 
 |-  ( y e. ( M [,] N ) -> ( A. x e. ( M [,] N ) A e. RR -> [_ y / x ]_ A e. RR ) )
30 24 29 mpan9 
 |-  ( ( ph /\ y e. ( M [,] N ) ) -> [_ y / x ]_ A e. RR )
31 19 30 syldan 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> [_ y / x ]_ A e. RR )
32 31 ralrimiva 
 |-  ( ph -> A. y e. ( M ... N ) [_ y / x ]_ A e. RR )
33 fzofzp1 
 |-  ( k e. ( M ..^ N ) -> ( k + 1 ) e. ( M ... N ) )
34 csbeq1 
 |-  ( y = ( k + 1 ) -> [_ y / x ]_ A = [_ ( k + 1 ) / x ]_ A )
35 34 eleq1d 
 |-  ( y = ( k + 1 ) -> ( [_ y / x ]_ A e. RR <-> [_ ( k + 1 ) / x ]_ A e. RR ) )
36 35 rspccva 
 |-  ( ( A. y e. ( M ... N ) [_ y / x ]_ A e. RR /\ ( k + 1 ) e. ( M ... N ) ) -> [_ ( k + 1 ) / x ]_ A e. RR )
37 32 33 36 syl2an 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> [_ ( k + 1 ) / x ]_ A e. RR )
38 elfzofz 
 |-  ( k e. ( M ..^ N ) -> k e. ( M ... N ) )
39 csbeq1 
 |-  ( y = k -> [_ y / x ]_ A = [_ k / x ]_ A )
40 39 eleq1d 
 |-  ( y = k -> ( [_ y / x ]_ A e. RR <-> [_ k / x ]_ A e. RR ) )
41 40 rspccva 
 |-  ( ( A. y e. ( M ... N ) [_ y / x ]_ A e. RR /\ k e. ( M ... N ) ) -> [_ k / x ]_ A e. RR )
42 32 38 41 syl2an 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> [_ k / x ]_ A e. RR )
43 37 42 resubcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) e. RR )
44 elfzoelz 
 |-  ( k e. ( M ..^ N ) -> k e. ZZ )
45 44 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. ZZ )
46 45 zred 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. RR )
47 46 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. CC )
48 ax-1cn 
 |-  1 e. CC
49 pncan2 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - k ) = 1 )
50 47 48 49 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( k + 1 ) - k ) = 1 )
51 50 oveq2d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. ( ( k + 1 ) - k ) ) = ( X x. 1 ) )
52 7 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. CC )
53 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
54 46 53 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. RR )
55 54 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. CC )
56 52 55 47 subdid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. ( ( k + 1 ) - k ) ) = ( ( X x. ( k + 1 ) ) - ( X x. k ) ) )
57 52 mulridd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( X x. 1 ) = X )
58 51 56 57 3eqtr3d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( X x. ( k + 1 ) ) - ( X x. k ) ) = X )
59 52 adantr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k [,] ( k + 1 ) ) ) -> X e. CC )
60 46 54 iccssred 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ RR )
61 ax-resscn 
 |-  RR C_ CC
62 60 61 sstrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ CC )
63 62 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k [,] ( k + 1 ) ) ) -> y e. CC )
64 ovmul 
 |-  ( ( X e. CC /\ y e. CC ) -> ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( X x. y ) )
65 59 63 64 syl2anc 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k [,] ( k + 1 ) ) ) -> ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( X x. y ) )
66 65 eqeq2d 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k [,] ( k + 1 ) ) ) -> ( z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) <-> z = ( X x. y ) ) )
67 66 pm5.32da 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) <-> ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X x. y ) ) ) )
68 67 opabbidv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X x. y ) ) } )
69 df-mpt 
 |-  ( y e. ( k [,] ( k + 1 ) ) |-> ( X x. y ) ) = { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X x. y ) ) }
70 68 69 eqtr4di 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( k [,] ( k + 1 ) ) |-> ( X x. y ) ) )
71 df-mpt 
 |-  ( y e. ( k [,] ( k + 1 ) ) |-> ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) = { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) }
72 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
73 72 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
74 61 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR C_ CC )
75 cncfmptc 
 |-  ( ( X e. RR /\ ( k [,] ( k + 1 ) ) C_ CC /\ RR C_ CC ) -> ( y e. ( k [,] ( k + 1 ) ) |-> X ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
76 7 62 74 75 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> X ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
77 cncfmptid 
 |-  ( ( ( k [,] ( k + 1 ) ) C_ RR /\ RR C_ CC ) -> ( y e. ( k [,] ( k + 1 ) ) |-> y ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
78 60 61 77 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> y ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
79 simpl 
 |-  ( ( X e. RR /\ y e. RR ) -> X e. RR )
80 79 recnd 
 |-  ( ( X e. RR /\ y e. RR ) -> X e. CC )
81 simpr 
 |-  ( ( X e. RR /\ y e. RR ) -> y e. RR )
82 81 recnd 
 |-  ( ( X e. RR /\ y e. RR ) -> y e. CC )
83 64 eqcomd 
 |-  ( ( X e. CC /\ y e. CC ) -> ( X x. y ) = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
84 80 82 83 syl2anc 
 |-  ( ( X e. RR /\ y e. RR ) -> ( X x. y ) = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
85 remulcl 
 |-  ( ( X e. RR /\ y e. RR ) -> ( X x. y ) e. RR )
86 84 85 eqeltrrd 
 |-  ( ( X e. RR /\ y e. RR ) -> ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR )
87 72 73 76 78 61 86 cncfmpt2ss 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
88 71 87 eqeltrrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> { <. y , z >. | ( y e. ( k [,] ( k + 1 ) ) /\ z = ( X ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
89 70 88 eqeltrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> ( X x. y ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
90 reelprrecn 
 |-  RR e. { RR , CC }
91 90 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR e. { RR , CC } )
92 12 zred 
 |-  ( ph -> M e. RR )
93 92 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR )
94 93 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR* )
95 elfzole1 
 |-  ( k e. ( M ..^ N ) -> M <_ k )
96 95 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M <_ k )
97 iooss1 
 |-  ( ( M e. RR* /\ M <_ k ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
98 94 96 97 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
99 14 zred 
 |-  ( ph -> N e. RR )
100 99 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR )
101 100 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR* )
102 33 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
103 elfzle2 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( k + 1 ) <_ N )
104 102 103 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) <_ N )
105 iooss2 
 |-  ( ( N e. RR* /\ ( k + 1 ) <_ N ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
106 101 104 105 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
107 98 106 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) N ) )
108 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
109 92 99 iccssred 
 |-  ( ph -> ( M [,] N ) C_ RR )
110 109 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ RR )
111 110 61 sstrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ CC )
112 108 111 sstrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) N ) C_ CC )
113 107 112 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ CC )
114 113 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> y e. CC )
115 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> 1 e. CC )
116 74 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. RR ) -> y e. CC )
117 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. RR ) -> 1 e. CC )
118 91 dvmptid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
119 ioossre 
 |-  ( k (,) ( k + 1 ) ) C_ RR
120 119 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ RR )
121 72 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
122 iooretop 
 |-  ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) )
123 122 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) ) )
124 91 116 117 118 120 121 72 123 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> y ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> 1 ) )
125 91 114 115 124 52 dvmptcmul 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. y ) ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. 1 ) ) )
126 57 mpteq2dv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. 1 ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> X ) )
127 125 126 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. y ) ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> X ) )
128 nfcv 
 |-  F/_ y A
129 128 25 27 cbvmpt 
 |-  ( x e. ( k [,] ( k + 1 ) ) |-> A ) = ( y e. ( k [,] ( k + 1 ) ) |-> [_ y / x ]_ A )
130 iccss 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ ( M <_ k /\ ( k + 1 ) <_ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
131 93 100 96 104 130 syl22anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
132 131 resmptd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> A ) |` ( k [,] ( k + 1 ) ) ) = ( x e. ( k [,] ( k + 1 ) ) |-> A ) )
133 2 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
134 rescncf 
 |-  ( ( k [,] ( k + 1 ) ) C_ ( M [,] N ) -> ( ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) -> ( ( x e. ( M [,] N ) |-> A ) |` ( k [,] ( k + 1 ) ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) ) )
135 131 133 134 sylc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> A ) |` ( k [,] ( k + 1 ) ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
136 132 135 eqeltrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( k [,] ( k + 1 ) ) |-> A ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
137 129 136 eqeltrrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> [_ y / x ]_ A ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
138 21 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
139 138 23 sylibr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M [,] N ) A e. RR )
140 108 sseli 
 |-  ( y e. ( M (,) N ) -> y e. ( M [,] N ) )
141 29 impcom 
 |-  ( ( A. x e. ( M [,] N ) A e. RR /\ y e. ( M [,] N ) ) -> [_ y / x ]_ A e. RR )
142 139 140 141 syl2an 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ A e. RR )
143 142 recnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ A e. CC )
144 108 sseli 
 |-  ( x e. ( M (,) N ) -> x e. ( M [,] N ) )
145 21 fvmptelcdm 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. RR )
146 145 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> A e. RR )
147 144 146 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> A e. RR )
148 147 fmpttd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR )
149 ioossre 
 |-  ( M (,) N ) C_ RR
150 dvfre 
 |-  ( ( ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR /\ ( M (,) N ) C_ RR ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
151 148 149 150 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
152 4 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
153 152 dmeqd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = dom ( x e. ( M (,) N ) |-> B ) )
154 3 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> B e. V )
155 154 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M (,) N ) B e. V )
156 dmmptg 
 |-  ( A. x e. ( M (,) N ) B e. V -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
157 155 156 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
158 153 157 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( M (,) N ) )
159 152 158 feq12d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR <-> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR ) )
160 151 159 mpbid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
161 eqid 
 |-  ( x e. ( M (,) N ) |-> B ) = ( x e. ( M (,) N ) |-> B )
162 161 fmpt 
 |-  ( A. x e. ( M (,) N ) B e. RR <-> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
163 160 162 sylibr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M (,) N ) B e. RR )
164 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
165 164 nfel1 
 |-  F/ x [_ y / x ]_ B e. RR
166 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
167 166 eleq1d 
 |-  ( x = y -> ( B e. RR <-> [_ y / x ]_ B e. RR ) )
168 165 167 rspc 
 |-  ( y e. ( M (,) N ) -> ( A. x e. ( M (,) N ) B e. RR -> [_ y / x ]_ B e. RR ) )
169 163 168 mpan9 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ B e. RR )
170 128 25 27 cbvmpt 
 |-  ( x e. ( M (,) N ) |-> A ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ A )
171 170 oveq2i 
 |-  ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( RR _D ( y e. ( M (,) N ) |-> [_ y / x ]_ A ) )
172 nfcv 
 |-  F/_ y B
173 172 164 166 cbvmpt 
 |-  ( x e. ( M (,) N ) |-> B ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ B )
174 152 171 173 3eqtr3g 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( M (,) N ) |-> [_ y / x ]_ A ) ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ B ) )
175 91 143 169 174 107 121 72 123 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> [_ y / x ]_ A ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> [_ y / x ]_ B ) )
176 8 anassrs 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> X <_ B )
177 176 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( k (,) ( k + 1 ) ) X <_ B )
178 nfcv 
 |-  F/_ x X
179 nfcv 
 |-  F/_ x <_
180 178 179 164 nfbr 
 |-  F/ x X <_ [_ y / x ]_ B
181 166 breq2d 
 |-  ( x = y -> ( X <_ B <-> X <_ [_ y / x ]_ B ) )
182 180 181 rspc 
 |-  ( y e. ( k (,) ( k + 1 ) ) -> ( A. x e. ( k (,) ( k + 1 ) ) X <_ B -> X <_ [_ y / x ]_ B ) )
183 177 182 mpan9 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> X <_ [_ y / x ]_ B )
184 46 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. RR* )
185 54 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. RR* )
186 46 lep1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k <_ ( k + 1 ) )
187 lbicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> k e. ( k [,] ( k + 1 ) ) )
188 184 185 186 187 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. ( k [,] ( k + 1 ) ) )
189 ubicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
190 184 185 186 189 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
191 oveq2 
 |-  ( y = k -> ( X x. y ) = ( X x. k ) )
192 oveq2 
 |-  ( y = ( k + 1 ) -> ( X x. y ) = ( X x. ( k + 1 ) ) )
193 46 54 89 127 137 175 183 188 190 186 191 39 192 34 dvle 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( X x. ( k + 1 ) ) - ( X x. k ) ) <_ ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
194 58 193 eqbrtrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X <_ ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
195 10 7 43 194 fsumle 
 |-  ( ph -> sum_ k e. ( M ..^ N ) X <_ sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
196 vex 
 |-  y e. _V
197 196 a1i 
 |-  ( y = M -> y e. _V )
198 eqeq2 
 |-  ( y = M -> ( x = y <-> x = M ) )
199 198 biimpa 
 |-  ( ( y = M /\ x = y ) -> x = M )
200 199 5 syl 
 |-  ( ( y = M /\ x = y ) -> A = C )
201 197 200 csbied 
 |-  ( y = M -> [_ y / x ]_ A = C )
202 196 a1i 
 |-  ( y = N -> y e. _V )
203 eqeq2 
 |-  ( y = N -> ( x = y <-> x = N ) )
204 203 biimpa 
 |-  ( ( y = N /\ x = y ) -> x = N )
205 204 6 syl 
 |-  ( ( y = N /\ x = y ) -> A = D )
206 202 205 csbied 
 |-  ( y = N -> [_ y / x ]_ A = D )
207 31 recnd 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> [_ y / x ]_ A e. CC )
208 39 34 201 206 1 207 telfsumo2 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) = ( D - C ) )
209 195 208 breqtrd 
 |-  ( ph -> sum_ k e. ( M ..^ N ) X <_ ( D - C ) )