Metamath Proof Explorer

Theorem dvfsumleOLD

Description: Obsolete version of dvfsumle as of 17-Apr-2025. (Contributed by Mario Carneiro, 14-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dvfsumleOLD.m 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 dvfsumleOLD.a 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
3 dvfsumleOLD.v 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )
4 dvfsumleOLD.b 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
5 dvfsumleOLD.c 
 |-  ( x = M -> A = C )
6 dvfsumleOLD.d 
 |-  ( x = N -> A = D )
7 dvfsumleOLD.x 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. RR )
8 dvfsumleOLD.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 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
60 59 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
61 12 zred 
 |-  ( ph -> M e. RR )
62 61 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR )
63 14 zred 
 |-  ( ph -> N e. RR )
64 63 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR )
65 elfzole1 
 |-  ( k e. ( M ..^ N ) -> M <_ k )
66 65 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M <_ k )
67 33 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
68 elfzle2 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( k + 1 ) <_ N )
69 67 68 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) <_ N )
70 iccss 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ ( M <_ k /\ ( k + 1 ) <_ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
71 62 64 66 69 70 syl22anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ ( M [,] N ) )
72 iccssre 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M [,] N ) C_ RR )
73 61 63 72 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ RR )
74 73 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ RR )
75 71 74 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ RR )
76 ax-resscn 
 |-  RR C_ CC
77 75 76 sstrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k [,] ( k + 1 ) ) C_ CC )
78 76 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR C_ CC )
79 cncfmptc 
 |-  ( ( X e. RR /\ ( k [,] ( k + 1 ) ) C_ CC /\ RR C_ CC ) -> ( y e. ( k [,] ( k + 1 ) ) |-> X ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
80 7 77 78 79 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> X ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
81 cncfmptid 
 |-  ( ( ( k [,] ( k + 1 ) ) C_ RR /\ RR C_ CC ) -> ( y e. ( k [,] ( k + 1 ) ) |-> y ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
82 75 76 81 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> y ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
83 remulcl 
 |-  ( ( X e. RR /\ y e. RR ) -> ( X x. y ) e. RR )
84 59 60 80 82 76 83 cncfmpt2ss 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> ( X x. y ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
85 reelprrecn 
 |-  RR e. { RR , CC }
86 85 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> RR e. { RR , CC } )
87 62 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR* )
88 iooss1 
 |-  ( ( M e. RR* /\ M <_ k ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
89 87 66 88 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
90 64 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR* )
91 iooss2 
 |-  ( ( N e. RR* /\ ( k + 1 ) <_ N ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
92 90 69 91 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
93 89 92 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) N ) )
94 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
95 74 76 sstrdi 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M [,] N ) C_ CC )
96 94 95 sstrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) N ) C_ CC )
97 93 96 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ CC )
98 97 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> y e. CC )
99 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> 1 e. CC )
100 78 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. RR ) -> y e. CC )
101 1cnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. RR ) -> 1 e. CC )
102 86 dvmptid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
103 ioossre 
 |-  ( k (,) ( k + 1 ) ) C_ RR
104 103 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ RR )
105 59 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
106 iooretop 
 |-  ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) )
107 106 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) e. ( topGen ` ran (,) ) )
108 86 100 101 102 104 105 59 107 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> y ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> 1 ) )
109 86 98 99 108 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 ) ) )
110 57 mpteq2dv 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. 1 ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> X ) )
111 109 110 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> ( X x. y ) ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> X ) )
112 nfcv 
 |-  F/_ y A
113 112 25 27 cbvmpt 
 |-  ( x e. ( k [,] ( k + 1 ) ) |-> A ) = ( y e. ( k [,] ( k + 1 ) ) |-> [_ y / x ]_ A )
114 71 resmptd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> A ) |` ( k [,] ( k + 1 ) ) ) = ( x e. ( k [,] ( k + 1 ) ) |-> A ) )
115 2 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
116 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 ) ) )
117 71 115 116 sylc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( x e. ( M [,] N ) |-> A ) |` ( k [,] ( k + 1 ) ) ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
118 114 117 eqeltrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( k [,] ( k + 1 ) ) |-> A ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
119 113 118 eqeltrrid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( y e. ( k [,] ( k + 1 ) ) |-> [_ y / x ]_ A ) e. ( ( k [,] ( k + 1 ) ) -cn-> RR ) )
120 21 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
121 120 23 sylibr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M [,] N ) A e. RR )
122 94 sseli 
 |-  ( y e. ( M (,) N ) -> y e. ( M [,] N ) )
123 29 impcom 
 |-  ( ( A. x e. ( M [,] N ) A e. RR /\ y e. ( M [,] N ) ) -> [_ y / x ]_ A e. RR )
124 121 122 123 syl2an 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ A e. RR )
125 124 recnd 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ A e. CC )
126 94 sseli 
 |-  ( x e. ( M (,) N ) -> x e. ( M [,] N ) )
127 21 fvmptelcdm 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. RR )
128 127 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> A e. RR )
129 126 128 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> A e. RR )
130 129 fmpttd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR )
131 ioossre 
 |-  ( M (,) N ) C_ RR
132 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 )
133 130 131 132 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
134 4 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
135 134 dmeqd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = dom ( x e. ( M (,) N ) |-> B ) )
136 3 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> B e. V )
137 136 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M (,) N ) B e. V )
138 dmmptg 
 |-  ( A. x e. ( M (,) N ) B e. V -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
139 137 138 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
140 135 139 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( M (,) N ) )
141 134 140 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 ) )
142 133 141 mpbid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
143 eqid 
 |-  ( x e. ( M (,) N ) |-> B ) = ( x e. ( M (,) N ) |-> B )
144 143 fmpt 
 |-  ( A. x e. ( M (,) N ) B e. RR <-> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
145 142 144 sylibr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M (,) N ) B e. RR )
146 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
147 146 nfel1 
 |-  F/ x [_ y / x ]_ B e. RR
148 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
149 148 eleq1d 
 |-  ( x = y -> ( B e. RR <-> [_ y / x ]_ B e. RR ) )
150 147 149 rspc 
 |-  ( y e. ( M (,) N ) -> ( A. x e. ( M (,) N ) B e. RR -> [_ y / x ]_ B e. RR ) )
151 145 150 mpan9 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( M (,) N ) ) -> [_ y / x ]_ B e. RR )
152 112 25 27 cbvmpt 
 |-  ( x e. ( M (,) N ) |-> A ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ A )
153 152 oveq2i 
 |-  ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( RR _D ( y e. ( M (,) N ) |-> [_ y / x ]_ A ) )
154 nfcv 
 |-  F/_ y B
155 154 146 148 cbvmpt 
 |-  ( x e. ( M (,) N ) |-> B ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ B )
156 134 153 155 3eqtr3g 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( M (,) N ) |-> [_ y / x ]_ A ) ) = ( y e. ( M (,) N ) |-> [_ y / x ]_ B ) )
157 86 125 151 156 93 105 59 107 dvmptres 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( y e. ( k (,) ( k + 1 ) ) |-> [_ y / x ]_ A ) ) = ( y e. ( k (,) ( k + 1 ) ) |-> [_ y / x ]_ B ) )
158 8 anassrs 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> X <_ B )
159 158 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( k (,) ( k + 1 ) ) X <_ B )
160 nfcv 
 |-  F/_ x X
161 nfcv 
 |-  F/_ x <_
162 160 161 146 nfbr 
 |-  F/ x X <_ [_ y / x ]_ B
163 148 breq2d 
 |-  ( x = y -> ( X <_ B <-> X <_ [_ y / x ]_ B ) )
164 162 163 rspc 
 |-  ( y e. ( k (,) ( k + 1 ) ) -> ( A. x e. ( k (,) ( k + 1 ) ) X <_ B -> X <_ [_ y / x ]_ B ) )
165 159 164 mpan9 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ y e. ( k (,) ( k + 1 ) ) ) -> X <_ [_ y / x ]_ B )
166 46 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. RR* )
167 54 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. RR* )
168 46 lep1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k <_ ( k + 1 ) )
169 lbicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> k e. ( k [,] ( k + 1 ) ) )
170 166 167 168 169 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. ( k [,] ( k + 1 ) ) )
171 ubicc2 
 |-  ( ( k e. RR* /\ ( k + 1 ) e. RR* /\ k <_ ( k + 1 ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
172 166 167 168 171 syl3anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( k [,] ( k + 1 ) ) )
173 oveq2 
 |-  ( y = k -> ( X x. y ) = ( X x. k ) )
174 oveq2 
 |-  ( y = ( k + 1 ) -> ( X x. y ) = ( X x. ( k + 1 ) ) )
175 46 54 84 111 119 157 165 170 172 168 173 39 174 34 dvle 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( X x. ( k + 1 ) ) - ( X x. k ) ) <_ ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
176 58 175 eqbrtrrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X <_ ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
177 10 7 43 176 fsumle 
 |-  ( ph -> sum_ k e. ( M ..^ N ) X <_ sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) )
178 vex 
 |-  y e. _V
179 178 a1i 
 |-  ( y = M -> y e. _V )
180 eqeq2 
 |-  ( y = M -> ( x = y <-> x = M ) )
181 180 biimpa 
 |-  ( ( y = M /\ x = y ) -> x = M )
182 181 5 syl 
 |-  ( ( y = M /\ x = y ) -> A = C )
183 179 182 csbied 
 |-  ( y = M -> [_ y / x ]_ A = C )
184 178 a1i 
 |-  ( y = N -> y e. _V )
185 eqeq2 
 |-  ( y = N -> ( x = y <-> x = N ) )
186 185 biimpa 
 |-  ( ( y = N /\ x = y ) -> x = N )
187 186 6 syl 
 |-  ( ( y = N /\ x = y ) -> A = D )
188 184 187 csbied 
 |-  ( y = N -> [_ y / x ]_ A = D )
189 31 recnd 
 |-  ( ( ph /\ y e. ( M ... N ) ) -> [_ y / x ]_ A e. CC )
190 39 34 183 188 1 189 telfsumo2 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( [_ ( k + 1 ) / x ]_ A - [_ k / x ]_ A ) = ( D - C ) )
191 177 190 breqtrd 
 |-  ( ph -> sum_ k e. ( M ..^ N ) X <_ ( D - C ) )