MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvfsumle Unicode version

Theorem dvfsumle 19766
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.)
Hypotheses
Ref Expression
dvfsumle.m  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
dvfsumle.a  |-  ( ph  ->  ( x  e.  ( M [,] N ) 
|->  A )  e.  ( ( M [,] N
) -cn-> RR ) )
dvfsumle.v  |-  ( (
ph  /\  x  e.  ( M (,) N ) )  ->  B  e.  V )
dvfsumle.b  |-  ( ph  ->  ( RR  _D  (
x  e.  ( M (,) N )  |->  A ) )  =  ( x  e.  ( M (,) N )  |->  B ) )
dvfsumle.c  |-  ( x  =  M  ->  A  =  C )
dvfsumle.d  |-  ( x  =  N  ->  A  =  D )
dvfsumle.x  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  X  e.  RR )
dvfsumle.l  |-  ( (
ph  /\  ( k  e.  ( M..^ N )  /\  x  e.  ( k (,) ( k  +  1 ) ) ) )  ->  X  <_  B )
Assertion
Ref Expression
dvfsumle  |-  ( ph  -> 
sum_ k  e.  ( M..^ N ) X  <_  ( D  -  C ) )
Distinct variable groups:    A, k    x, k, M    k, N, x    ph, k, x    x, X    x, C    x, D    x, V
Allowed substitution hints:    A( x)    B( x, k)    C( k)    D( k)    V( k)    X( k)

Proof of Theorem dvfsumle
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 fzofi 11234 . . . 4  |-  ( M..^ N )  e.  Fin
21a1i 11 . . 3  |-  ( ph  ->  ( M..^ N )  e.  Fin )
3 dvfsumle.x . . 3  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  X  e.  RR )
4 dvfsumle.m . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
5 eluzel2 10419 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
64, 5syl 16 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ZZ )
7 eluzelz 10422 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
84, 7syl 16 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ZZ )
9 fzval2 10972 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M ... N
)  =  ( ( M [,] N )  i^i  ZZ ) )
106, 8, 9syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( M ... N
)  =  ( ( M [,] N )  i^i  ZZ ) )
11 inss1 3498 . . . . . . . . 9  |-  ( ( M [,] N )  i^i  ZZ )  C_  ( M [,] N )
1210, 11syl6eqss 3335 . . . . . . . 8  |-  ( ph  ->  ( M ... N
)  C_  ( M [,] N ) )
1312sselda 3285 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( M ... N ) )  ->  y  e.  ( M [,] N ) )
14 dvfsumle.a . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( M [,] N ) 
|->  A )  e.  ( ( M [,] N
) -cn-> RR ) )
15 cncff 18788 . . . . . . . . . 10  |-  ( ( x  e.  ( M [,] N )  |->  A )  e.  ( ( M [,] N )
-cn-> RR )  ->  (
x  e.  ( M [,] N )  |->  A ) : ( M [,] N ) --> RR )
1614, 15syl 16 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( M [,] N ) 
|->  A ) : ( M [,] N ) --> RR )
17 eqid 2381 . . . . . . . . . 10  |-  ( x  e.  ( M [,] N )  |->  A )  =  ( x  e.  ( M [,] N
)  |->  A )
1817fmpt 5823 . . . . . . . . 9  |-  ( A. x  e.  ( M [,] N ) A  e.  RR  <->  ( x  e.  ( M [,] N
)  |->  A ) : ( M [,] N
) --> RR )
1916, 18sylibr 204 . . . . . . . 8  |-  ( ph  ->  A. x  e.  ( M [,] N ) A  e.  RR )
20 nfcsb1v 3220 . . . . . . . . . 10  |-  F/_ x [_ y  /  x ]_ A
2120nfel1 2527 . . . . . . . . 9  |-  F/ x [_ y  /  x ]_ A  e.  RR
22 csbeq1a 3196 . . . . . . . . . 10  |-  ( x  =  y  ->  A  =  [_ y  /  x ]_ A )
2322eleq1d 2447 . . . . . . . . 9  |-  ( x  =  y  ->  ( A  e.  RR  <->  [_ y  /  x ]_ A  e.  RR ) )
2421, 23rspc 2983 . . . . . . . 8  |-  ( y  e.  ( M [,] N )  ->  ( A. x  e.  ( M [,] N ) A  e.  RR  ->  [_ y  /  x ]_ A  e.  RR ) )
2519, 24mpan9 456 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( M [,] N ) )  ->  [_ y  /  x ]_ A  e.  RR )
2613, 25syldan 457 . . . . . 6  |-  ( (
ph  /\  y  e.  ( M ... N ) )  ->  [_ y  /  x ]_ A  e.  RR )
2726ralrimiva 2726 . . . . 5  |-  ( ph  ->  A. y  e.  ( M ... N )
[_ y  /  x ]_ A  e.  RR )
28 fzofzp1 11110 . . . . 5  |-  ( k  e.  ( M..^ N
)  ->  ( k  +  1 )  e.  ( M ... N
) )
29 csbeq1 3191 . . . . . . 7  |-  ( y  =  ( k  +  1 )  ->  [_ y  /  x ]_ A  = 
[_ ( k  +  1 )  /  x ]_ A )
3029eleq1d 2447 . . . . . 6  |-  ( y  =  ( k  +  1 )  ->  ( [_ y  /  x ]_ A  e.  RR  <->  [_ ( k  +  1 )  /  x ]_ A  e.  RR )
)
3130rspccva 2988 . . . . 5  |-  ( ( A. y  e.  ( M ... N )
[_ y  /  x ]_ A  e.  RR  /\  ( k  +  1 )  e.  ( M ... N ) )  ->  [_ ( k  +  1 )  /  x ]_ A  e.  RR )
3227, 28, 31syl2an 464 . . . 4  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  [_ ( k  +  1 )  /  x ]_ A  e.  RR )
33 elfzofz 11078 . . . . 5  |-  ( k  e.  ( M..^ N
)  ->  k  e.  ( M ... N ) )
34 csbeq1 3191 . . . . . . 7  |-  ( y  =  k  ->  [_ y  /  x ]_ A  = 
[_ k  /  x ]_ A )
3534eleq1d 2447 . . . . . 6  |-  ( y  =  k  ->  ( [_ y  /  x ]_ A  e.  RR  <->  [_ k  /  x ]_ A  e.  RR )
)
3635rspccva 2988 . . . . 5  |-  ( ( A. y  e.  ( M ... N )
[_ y  /  x ]_ A  e.  RR  /\  k  e.  ( M ... N ) )  ->  [_ k  /  x ]_ A  e.  RR )
3727, 33, 36syl2an 464 . . . 4  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  [_ k  /  x ]_ A  e.  RR )
3832, 37resubcld 9391 . . 3  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( [_ (
k  +  1 )  /  x ]_ A  -  [_ k  /  x ]_ A )  e.  RR )
39 elfzoelz 11064 . . . . . . . . . 10  |-  ( k  e.  ( M..^ N
)  ->  k  e.  ZZ )
4039adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  e.  ZZ )
4140zred 10301 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  e.  RR )
4241recnd 9041 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  e.  CC )
43 ax-1cn 8975 . . . . . . 7  |-  1  e.  CC
44 pncan2 9238 . . . . . . 7  |-  ( ( k  e.  CC  /\  1  e.  CC )  ->  ( ( k  +  1 )  -  k
)  =  1 )
4542, 43, 44sylancl 644 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( ( k  +  1 )  -  k )  =  1 )
4645oveq2d 6030 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( X  x.  ( ( k  +  1 )  -  k
) )  =  ( X  x.  1 ) )
473recnd 9041 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  X  e.  CC )
48 peano2re 9165 . . . . . . . 8  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
4941, 48syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  e.  RR )
5049recnd 9041 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  e.  CC )
5147, 50, 42subdid 9415 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( X  x.  ( ( k  +  1 )  -  k
) )  =  ( ( X  x.  (
k  +  1 ) )  -  ( X  x.  k ) ) )
5247mulid1d 9032 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( X  x.  1 )  =  X )
5346, 51, 523eqtr3d 2421 . . . 4  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( ( X  x.  ( k  +  1 ) )  -  ( X  x.  k
) )  =  X )
54 eqid 2381 . . . . . 6  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5554mulcn 18762 . . . . . 6  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
566zred 10301 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
5756adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  M  e.  RR )
588zred 10301 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  RR )
5958adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  N  e.  RR )
60 elfzole1 11071 . . . . . . . . . . 11  |-  ( k  e.  ( M..^ N
)  ->  M  <_  k )
6160adantl 453 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  M  <_  k
)
6228adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  e.  ( M ... N ) )
63 elfzle2 10987 . . . . . . . . . . 11  |-  ( ( k  +  1 )  e.  ( M ... N )  ->  (
k  +  1 )  <_  N )
6462, 63syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  <_  N
)
65 iccss 10904 . . . . . . . . . 10  |-  ( ( ( M  e.  RR  /\  N  e.  RR )  /\  ( M  <_ 
k  /\  ( k  +  1 )  <_  N ) )  -> 
( k [,] (
k  +  1 ) )  C_  ( M [,] N ) )
6657, 59, 61, 64, 65syl22anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k [,] ( k  +  1 ) )  C_  ( M [,] N ) )
67 iccssre 10918 . . . . . . . . . . 11  |-  ( ( M  e.  RR  /\  N  e.  RR )  ->  ( M [,] N
)  C_  RR )
6856, 58, 67syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( M [,] N
)  C_  RR )
6968adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( M [,] N )  C_  RR )
7066, 69sstrd 3295 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k [,] ( k  +  1 ) )  C_  RR )
71 ax-resscn 8974 . . . . . . . 8  |-  RR  C_  CC
7270, 71syl6ss 3297 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k [,] ( k  +  1 ) )  C_  CC )
7371a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  RR  C_  CC )
74 cncfmptc 18806 . . . . . . 7  |-  ( ( X  e.  RR  /\  ( k [,] (
k  +  1 ) )  C_  CC  /\  RR  C_  CC )  ->  (
y  e.  ( k [,] ( k  +  1 ) )  |->  X )  e.  ( ( k [,] ( k  +  1 ) )
-cn-> RR ) )
753, 72, 73, 74syl3anc 1184 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( y  e.  ( k [,] (
k  +  1 ) )  |->  X )  e.  ( ( k [,] ( k  +  1 ) ) -cn-> RR ) )
76 cncfmptid 18807 . . . . . . 7  |-  ( ( ( k [,] (
k  +  1 ) )  C_  RR  /\  RR  C_  CC )  ->  (
y  e.  ( k [,] ( k  +  1 ) )  |->  y )  e.  ( ( k [,] ( k  +  1 ) )
-cn-> RR ) )
7770, 71, 76sylancl 644 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( y  e.  ( k [,] (
k  +  1 ) )  |->  y )  e.  ( ( k [,] ( k  +  1 ) ) -cn-> RR ) )
78 remulcl 9002 . . . . . 6  |-  ( ( X  e.  RR  /\  y  e.  RR )  ->  ( X  x.  y
)  e.  RR )
7954, 55, 75, 77, 71, 78cncfmpt2ss 18810 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( y  e.  ( k [,] (
k  +  1 ) )  |->  ( X  x.  y ) )  e.  ( ( k [,] ( k  +  1 ) ) -cn-> RR ) )
80 reex 9008 . . . . . . . . 9  |-  RR  e.  _V
8180prid1 3849 . . . . . . . 8  |-  RR  e.  { RR ,  CC }
8281a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  RR  e.  { RR ,  CC } )
8357rexrd 9061 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  M  e.  RR* )
84 iooss1 10877 . . . . . . . . . . 11  |-  ( ( M  e.  RR*  /\  M  <_  k )  ->  (
k (,) ( k  +  1 ) ) 
C_  ( M (,) ( k  +  1 ) ) )
8583, 61, 84syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k (,) ( k  +  1 ) )  C_  ( M (,) ( k  +  1 ) ) )
8659rexrd 9061 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  N  e.  RR* )
87 iooss2 10878 . . . . . . . . . . 11  |-  ( ( N  e.  RR*  /\  (
k  +  1 )  <_  N )  -> 
( M (,) (
k  +  1 ) )  C_  ( M (,) N ) )
8886, 64, 87syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( M (,) ( k  +  1 ) )  C_  ( M (,) N ) )
8985, 88sstrd 3295 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k (,) ( k  +  1 ) )  C_  ( M (,) N ) )
90 ioossicc 10922 . . . . . . . . . 10  |-  ( M (,) N )  C_  ( M [,] N )
9169, 71syl6ss 3297 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( M [,] N )  C_  CC )
9290, 91syl5ss 3296 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( M (,) N )  C_  CC )
9389, 92sstrd 3295 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k (,) ( k  +  1 ) )  C_  CC )
9493sselda 3285 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( k (,) (
k  +  1 ) ) )  ->  y  e.  CC )
9543a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( k (,) (
k  +  1 ) ) )  ->  1  e.  CC )
9673sselda 3285 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  RR )  ->  y  e.  CC )
9743a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  RR )  ->  1  e.  CC )
9882dvmptid 19704 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  RR  |->  y ) )  =  ( y  e.  RR  |->  1 ) )
99 ioossre 10898 . . . . . . . . 9  |-  ( k (,) ( k  +  1 ) )  C_  RR
10099a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k (,) ( k  +  1 ) )  C_  RR )
10154tgioo2 18699 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
102 iooretop 18665 . . . . . . . . 9  |-  ( k (,) ( k  +  1 ) )  e.  ( topGen `  ran  (,) )
103102a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k (,) ( k  +  1 ) )  e.  (
topGen `  ran  (,) )
)
10482, 96, 97, 98, 100, 101, 54, 103dvmptres 19710 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  y ) )  =  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  1 ) )
10582, 94, 95, 104, 47dvmptcmul 19711 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  ( X  x.  y
) ) )  =  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  ( X  x.  1 ) ) )
10652mpteq2dv 4231 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( y  e.  ( k (,) (
k  +  1 ) )  |->  ( X  x.  1 ) )  =  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  X ) )
107105, 106eqtrd 2413 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  ( X  x.  y
) ) )  =  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  X ) )
108 nfcv 2517 . . . . . . 7  |-  F/_ y A
109108, 20, 22cbvmpt 4234 . . . . . 6  |-  ( x  e.  ( k [,] ( k  +  1 ) )  |->  A )  =  ( y  e.  ( k [,] (
k  +  1 ) )  |->  [_ y  /  x ]_ A )
110 resmpt 5125 . . . . . . . 8  |-  ( ( k [,] ( k  +  1 ) ) 
C_  ( M [,] N )  ->  (
( x  e.  ( M [,] N ) 
|->  A )  |`  (
k [,] ( k  +  1 ) ) )  =  ( x  e.  ( k [,] ( k  +  1 ) )  |->  A ) )
11166, 110syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( ( x  e.  ( M [,] N )  |->  A )  |`  ( k [,] (
k  +  1 ) ) )  =  ( x  e.  ( k [,] ( k  +  1 ) )  |->  A ) )
11214adantr 452 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( x  e.  ( M [,] N
)  |->  A )  e.  ( ( M [,] N ) -cn-> RR ) )
113 rescncf 18792 . . . . . . . 8  |-  ( ( 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 ) ) )
11466, 112, 113sylc 58 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( ( x  e.  ( M [,] N )  |->  A )  |`  ( k [,] (
k  +  1 ) ) )  e.  ( ( k [,] (
k  +  1 ) ) -cn-> RR ) )
115111, 114eqeltrrd 2456 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( x  e.  ( k [,] (
k  +  1 ) )  |->  A )  e.  ( ( k [,] ( k  +  1 ) ) -cn-> RR ) )
116109, 115syl5eqelr 2466 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( y  e.  ( k [,] (
k  +  1 ) )  |->  [_ y  /  x ]_ A )  e.  ( ( k [,] (
k  +  1 ) ) -cn-> RR ) )
11716adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( x  e.  ( M [,] N
)  |->  A ) : ( M [,] N
) --> RR )
118117, 18sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  A. x  e.  ( M [,] N ) A  e.  RR )
11990sseli 3281 . . . . . . . 8  |-  ( y  e.  ( M (,) N )  ->  y  e.  ( M [,] N
) )
12024impcom 420 . . . . . . . 8  |-  ( ( A. x  e.  ( M [,] N ) A  e.  RR  /\  y  e.  ( M [,] N ) )  ->  [_ y  /  x ]_ A  e.  RR )
121118, 119, 120syl2an 464 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( M (,) N
) )  ->  [_ y  /  x ]_ A  e.  RR )
122121recnd 9041 . . . . . 6  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( M (,) N
) )  ->  [_ y  /  x ]_ A  e.  CC )
12390sseli 3281 . . . . . . . . . . . 12  |-  ( x  e.  ( M (,) N )  ->  x  e.  ( M [,] N
) )
12419r19.21bi 2741 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( M [,] N ) )  ->  A  e.  RR )
125124adantlr 696 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  x  e.  ( M [,] N
) )  ->  A  e.  RR )
126123, 125sylan2 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  x  e.  ( M (,) N
) )  ->  A  e.  RR )
127 eqid 2381 . . . . . . . . . . 11  |-  ( x  e.  ( M (,) N )  |->  A )  =  ( x  e.  ( M (,) N
)  |->  A )
128126, 127fmptd 5826 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( x  e.  ( M (,) N
)  |->  A ) : ( M (,) N
) --> RR )
129 ioossre 10898 . . . . . . . . . 10  |-  ( M (,) N )  C_  RR
130 dvfre 19698 . . . . . . . . . 10  |-  ( ( ( 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 )
131128, 129, 130sylancl 644 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( x  e.  ( M (,) N )  |->  A ) ) : dom  ( RR  _D  (
x  e.  ( M (,) N )  |->  A ) ) --> RR )
132 dvfsumle.b . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
x  e.  ( M (,) N )  |->  A ) )  =  ( x  e.  ( M (,) N )  |->  B ) )
133132adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( x  e.  ( M (,) N )  |->  A ) )  =  ( x  e.  ( M (,) N )  |->  B ) )
134133dmeqd 5006 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  dom  ( RR  _D  ( x  e.  ( M (,) N ) 
|->  A ) )  =  dom  ( x  e.  ( M (,) N
)  |->  B ) )
135 dvfsumle.v . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( M (,) N ) )  ->  B  e.  V )
136135adantlr 696 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  x  e.  ( M (,) N
) )  ->  B  e.  V )
137136ralrimiva 2726 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  A. x  e.  ( M (,) N ) B  e.  V )
138 dmmptg 5301 . . . . . . . . . . . 12  |-  ( A. x  e.  ( M (,) N ) B  e.  V  ->  dom  ( x  e.  ( M (,) N )  |->  B )  =  ( M (,) N ) )
139137, 138syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  dom  ( x  e.  ( M (,) N
)  |->  B )  =  ( M (,) N
) )
140134, 139eqtrd 2413 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  dom  ( RR  _D  ( x  e.  ( M (,) N ) 
|->  A ) )  =  ( M (,) N
) )
141133, 140feq12d 5516 . . . . . . . . 9  |-  ( (
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 ) )
142131, 141mpbid 202 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( x  e.  ( M (,) N
)  |->  B ) : ( M (,) N
) --> RR )
143 eqid 2381 . . . . . . . . 9  |-  ( x  e.  ( M (,) N )  |->  B )  =  ( x  e.  ( M (,) N
)  |->  B )
144143fmpt 5823 . . . . . . . 8  |-  ( A. x  e.  ( M (,) N ) B  e.  RR  <->  ( x  e.  ( M (,) N
)  |->  B ) : ( M (,) N
) --> RR )
145142, 144sylibr 204 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  A. x  e.  ( M (,) N ) B  e.  RR )
146 nfcsb1v 3220 . . . . . . . . 9  |-  F/_ x [_ y  /  x ]_ B
147146nfel1 2527 . . . . . . . 8  |-  F/ x [_ y  /  x ]_ B  e.  RR
148 csbeq1a 3196 . . . . . . . . 9  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
149148eleq1d 2447 . . . . . . . 8  |-  ( x  =  y  ->  ( B  e.  RR  <->  [_ y  /  x ]_ B  e.  RR ) )
150147, 149rspc 2983 . . . . . . 7  |-  ( y  e.  ( M (,) N )  ->  ( A. x  e.  ( M (,) N ) B  e.  RR  ->  [_ y  /  x ]_ B  e.  RR ) )
151145, 150mpan9 456 . . . . . 6  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( M (,) N
) )  ->  [_ y  /  x ]_ B  e.  RR )
152108, 20, 22cbvmpt 4234 . . . . . . . 8  |-  ( x  e.  ( M (,) N )  |->  A )  =  ( y  e.  ( M (,) N
)  |->  [_ y  /  x ]_ A )
153152oveq2i 6025 . . . . . . 7  |-  ( RR 
_D  ( x  e.  ( M (,) N
)  |->  A ) )  =  ( RR  _D  ( y  e.  ( M (,) N ) 
|->  [_ y  /  x ]_ A ) )
154 nfcv 2517 . . . . . . . 8  |-  F/_ y B
155154, 146, 148cbvmpt 4234 . . . . . . 7  |-  ( x  e.  ( M (,) N )  |->  B )  =  ( y  e.  ( M (,) N
)  |->  [_ y  /  x ]_ B )
156133, 153, 1553eqtr3g 2436 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  ( M (,) N ) 
|->  [_ y  /  x ]_ A ) )  =  ( y  e.  ( M (,) N ) 
|->  [_ y  /  x ]_ B ) )
15782, 122, 151, 156, 89, 101, 54, 103dvmptres 19710 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( RR  _D  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  [_ y  /  x ]_ A ) )  =  ( y  e.  ( k (,) ( k  +  1 ) ) 
|->  [_ y  /  x ]_ B ) )
158 dvfsumle.l . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  ( M..^ N )  /\  x  e.  ( k (,) ( k  +  1 ) ) ) )  ->  X  <_  B )
159158anassrs 630 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  x  e.  ( k (,) (
k  +  1 ) ) )  ->  X  <_  B )
160159ralrimiva 2726 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  A. x  e.  ( k (,) ( k  +  1 ) ) X  <_  B )
161 nfcv 2517 . . . . . . . 8  |-  F/_ x X
162 nfcv 2517 . . . . . . . 8  |-  F/_ x  <_
163161, 162, 146nfbr 4191 . . . . . . 7  |-  F/ x  X  <_  [_ y  /  x ]_ B
164148breq2d 4159 . . . . . . 7  |-  ( x  =  y  ->  ( X  <_  B  <->  X  <_  [_ y  /  x ]_ B ) )
165163, 164rspc 2983 . . . . . 6  |-  ( y  e.  ( k (,) ( k  +  1 ) )  ->  ( A. x  e.  (
k (,) ( k  +  1 ) ) X  <_  B  ->  X  <_  [_ y  /  x ]_ B ) )
166160, 165mpan9 456 . . . . 5  |-  ( ( ( ph  /\  k  e.  ( M..^ N ) )  /\  y  e.  ( k (,) (
k  +  1 ) ) )  ->  X  <_  [_ y  /  x ]_ B )
16741rexrd 9061 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  e.  RR* )
16849rexrd 9061 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  e.  RR* )
16941lep1d 9868 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  <_  (
k  +  1 ) )
170 lbicc2 10939 . . . . . 6  |-  ( ( k  e.  RR*  /\  (
k  +  1 )  e.  RR*  /\  k  <_  ( k  +  1 ) )  ->  k  e.  ( k [,] (
k  +  1 ) ) )
171167, 168, 169, 170syl3anc 1184 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  k  e.  ( k [,] ( k  +  1 ) ) )
172 ubicc2 10940 . . . . . 6  |-  ( ( k  e.  RR*  /\  (
k  +  1 )  e.  RR*  /\  k  <_  ( k  +  1 ) )  ->  (
k  +  1 )  e.  ( k [,] ( k  +  1 ) ) )
173167, 168, 169, 172syl3anc 1184 . . . . 5  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( k  +  1 )  e.  ( k [,] ( k  +  1 ) ) )
174 oveq2 6022 . . . . 5  |-  ( y  =  k  ->  ( X  x.  y )  =  ( X  x.  k ) )
175 oveq2 6022 . . . . 5  |-  ( y  =  ( k  +  1 )  ->  ( X  x.  y )  =  ( X  x.  ( k  +  1 ) ) )
17641, 49, 79, 107, 116, 157, 166, 171, 173, 169, 174, 34, 175, 29dvle 19752 . . . 4  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  ( ( X  x.  ( k  +  1 ) )  -  ( X  x.  k
) )  <_  ( [_ ( k  +  1 )  /  x ]_ A  -  [_ k  /  x ]_ A ) )
17753, 176eqbrtrrd 4169 . . 3  |-  ( (
ph  /\  k  e.  ( M..^ N ) )  ->  X  <_  ( [_ ( k  +  1 )  /  x ]_ A  -  [_ k  /  x ]_ A ) )
1782, 3, 38, 177fsumle 12499 . 2  |-  ( ph  -> 
sum_ k  e.  ( M..^ N ) X  <_  sum_ k  e.  ( M..^ N ) (
[_ ( k  +  1 )  /  x ]_ A  -  [_ k  /  x ]_ A ) )
179 vex 2896 . . . . 5  |-  y  e. 
_V
180179a1i 11 . . . 4  |-  ( y  =  M  ->  y  e.  _V )
181 eqeq2 2390 . . . . . 6  |-  ( y  =  M  ->  (
x  =  y  <->  x  =  M ) )
182181biimpa 471 . . . . 5  |-  ( ( y  =  M  /\  x  =  y )  ->  x  =  M )
183 dvfsumle.c . . . . 5  |-  ( x  =  M  ->  A  =  C )
184182, 183syl 16 . . . 4  |-  ( ( y  =  M  /\  x  =  y )  ->  A  =  C )
185180, 184csbied 3230 . . 3  |-  ( y  =  M  ->  [_ y  /  x ]_ A  =  C )
186179a1i 11 . . . 4  |-  ( y  =  N  ->  y  e.  _V )
187 eqeq2 2390 . . . . . 6  |-  ( y  =  N  ->  (
x  =  y  <->  x  =  N ) )
188187biimpa 471 . . . . 5  |-  ( ( y  =  N  /\  x  =  y )  ->  x  =  N )
189 dvfsumle.d . . . . 5  |-  ( x  =  N  ->  A  =  D )
190188, 189syl 16 . . . 4  |-  ( ( y  =  N  /\  x  =  y )  ->  A  =  D )
191186, 190csbied 3230 . . 3  |-  ( y  =  N  ->  [_ y  /  x ]_ A  =  D )
19226recnd 9041 . . 3  |-  ( (
ph  /\  y  e.  ( M ... N ) )  ->  [_ y  /  x ]_ A  e.  CC )
19334, 29, 185, 191, 4, 192fsumtscopo2 12503 . 2  |-  ( ph  -> 
sum_ k  e.  ( M..^ N ) (
[_ ( k  +  1 )  /  x ]_ A  -  [_ k  /  x ]_ A )  =  ( D  -  C ) )
194178, 193breqtrd 4171 1  |-  ( ph  -> 
sum_ k  e.  ( M..^ N ) X  <_  ( D  -  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2643   _Vcvv 2893   [_csb 3188    i^i cin 3256    C_ wss 3257   {cpr 3752   class class class wbr 4147    e. cmpt 4201   dom cdm 4812   ran crn 4813    |` cres 4814   -->wf 5384   ` cfv 5388  (class class class)co 6014   Fincfn 7039   CCcc 8915   RRcr 8916   1c1 8918    + caddc 8920    x. cmul 8922   RR*cxr 9046    <_ cle 9048    - cmin 9217   ZZcz 10208   ZZ>=cuz 10414   (,)cioo 10842   [,]cicc 10845   ...cfz 10969  ..^cfzo 11059   sum_csu 12400   TopOpenctopn 13570   topGenctg 13586  ℂfldccnfld 16620   -cn->ccncf 18771    _D cdv 19611
This theorem is referenced by:  dvfsumge  19767
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362  ax-rep 4255  ax-sep 4265  ax-nul 4273  ax-pow 4312  ax-pr 4338  ax-un 4635  ax-inf2 7523  ax-cnex 8973  ax-resscn 8974  ax-1cn 8975  ax-icn 8976  ax-addcl 8977  ax-addrcl 8978  ax-mulcl 8979  ax-mulrcl 8980  ax-mulcom 8981  ax-addass 8982  ax-mulass 8983  ax-distr 8984  ax-i2m1 8985  ax-1ne0 8986  ax-1rid 8987  ax-rnegex 8988  ax-rrecex 8989  ax-cnre 8990  ax-pre-lttri 8991  ax-pre-lttrn 8992  ax-pre-ltadd 8993  ax-pre-mulgt0 8994  ax-pre-sup 8995  ax-addf 8996  ax-mulf 8997
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2236  df-mo 2237  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ne 2546  df-nel 2547  df-ral 2648  df-rex 2649  df-reu 2650  df-rmo 2651  df-rab 2652  df-v 2895  df-sbc 3099  df-csb 3189  df-dif 3260  df-un 3262  df-in 3264  df-ss 3271  df-pss 3273  df-nul 3566  df-if 3677  df-pw 3738  df-sn 3757  df-pr 3758  df-tp 3759  df-op 3760  df-uni 3952  df-int 3987  df-iun 4031  df-iin 4032  df-br 4148  df-opab 4202  df-mpt 4203  df-tr 4238  df-eprel 4429  df-id 4433  df-po 4438  df-so 4439  df-fr 4476  df-se 4477  df-we 4478  df-ord 4519  df-on 4520  df-lim 4521  df-suc 4522  df-om 4780  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5352  df-fun 5390  df-fn 5391  df-f 5392  df-f1 5393  df-fo 5394  df-f1o 5395  df-fv 5396  df-isom 5397  df-ov 6017  df-oprab 6018  df-mpt2 6019  df-of 6238  df-1st 6282  df-2nd 6283  df-riota 6479  df-recs 6563  df-rdg 6598  df-1o 6654  df-2o 6655  df-oadd 6658  df-er 6835  df-map 6950  df-pm 6951  df-ixp 6994  df-en 7040  df-dom 7041  df-sdom 7042  df-fin 7043  df-fi 7345  df-sup 7375  df-oi 7406  df-card 7753  df-cda 7975  df-pnf 9049  df-mnf 9050  df-xr 9051  df-ltxr 9052  df-le 9053  df-sub 9219  df-neg 9220  df-div 9604  df-nn 9927  df-2 9984  df-3 9985  df-4 9986  df-5 9987  df-6 9988  df-7 9989  df-8 9990  df-9 9991  df-10 9992  df-n0 10148  df-z 10209  df-dec 10309  df-uz 10415  df-q 10501  df-rp 10539  df-xneg 10636  df-xadd 10637  df-xmul 10638  df-ioo 10846  df-ico 10848  df-icc 10849  df-fz 10970  df-fzo 11060  df-seq 11245  df-exp 11304  df-hash 11540  df-cj 11825  df-re 11826  df-im 11827  df-sqr 11961  df-abs 11962  df-clim 12203  df-sum 12401  df-struct 13392  df-ndx 13393  df-slot 13394  df-base 13395  df-sets 13396  df-ress 13397  df-plusg 13463  df-mulr 13464  df-starv 13465  df-sca 13466  df-vsca 13467  df-tset 13469  df-ple 13470  df-ds 13472  df-unif 13473  df-hom 13474  df-cco 13475  df-rest 13571  df-topn 13572  df-topgen 13588  df-pt 13589  df-prds 13592  df-xrs 13647  df-0g 13648  df-gsum 13649  df-qtop 13654  df-imas 13655  df-xps 13657  df-mre 13732  df-mrc 13733  df-acs 13735  df-mnd 14611  df-submnd 14660  df-mulg 14736  df-cntz 15037  df-cmn 15335  df-xmet 16613  df-met 16614  df-bl 16615  df-mopn 16616  df-fbas 16617  df-fg 16618  df-cnfld 16621  df-top 16880  df-bases 16882  df-topon 16883  df-topsp 16884  df-cld 17000  df-ntr 17001  df-cls 17002  df-nei 17079  df-lp 17117  df-perf 17118  df-cn 17207  df-cnp 17208  df-haus 17295  df-cmp 17366  df-tx 17509  df-hmeo 17702  df-fil 17793  df-fm 17885  df-flim 17886  df-flf 17887  df-xms 18253  df-ms 18254  df-tms 18255  df-cncf 18773  df-limc 19614  df-dv 19615
  Copyright terms: Public domain W3C validator