Metamath Proof Explorer

Theorem dvfsumge

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 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 )
dvfsumge.l 
|- ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> B <_ X )
Assertion dvfsumge 
|- ( ph -> ( D - C ) <_ sum_ k e. ( M ..^ N ) X )

Proof

Step Hyp Ref Expression
1 dvfsumle.m 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 dvfsumle.a 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) )
3 dvfsumle.v 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> B e. V )
4 dvfsumle.b 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
5 dvfsumle.c 
 |-  ( x = M -> A = C )
6 dvfsumle.d 
 |-  ( x = N -> A = D )
7 dvfsumle.x 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. RR )
8 dvfsumge.l 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> B <_ X )
9 df-neg 
 |-  -u A = ( 0 - A )
10 9 mpteq2i 
 |-  ( x e. ( M [,] N ) |-> -u A ) = ( x e. ( M [,] N ) |-> ( 0 - A ) )
11 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 11 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
13 0red 
 |-  ( ph -> 0 e. RR )
14 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
15 1 14 syl 
 |-  ( ph -> M e. ZZ )
16 15 zred 
 |-  ( ph -> M e. RR )
17 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
18 1 17 syl 
 |-  ( ph -> N e. ZZ )
19 18 zred 
 |-  ( ph -> N e. RR )
20 iccssre 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M [,] N ) C_ RR )
21 16 19 20 syl2anc 
 |-  ( ph -> ( M [,] N ) C_ RR )
22 ax-resscn 
 |-  RR C_ CC
23 21 22 sstrdi 
 |-  ( ph -> ( M [,] N ) C_ CC )
24 22 a1i 
 |-  ( ph -> RR C_ CC )
25 cncfmptc 
 |-  ( ( 0 e. RR /\ ( M [,] N ) C_ CC /\ RR C_ CC ) -> ( x e. ( M [,] N ) |-> 0 ) e. ( ( M [,] N ) -cn-> RR ) )
26 13 23 24 25 syl3anc 
 |-  ( ph -> ( x e. ( M [,] N ) |-> 0 ) e. ( ( M [,] N ) -cn-> RR ) )
27 resubcl 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 - A ) e. RR )
28 11 12 26 2 22 27 cncfmpt2ss 
 |-  ( ph -> ( x e. ( M [,] N ) |-> ( 0 - A ) ) e. ( ( M [,] N ) -cn-> RR ) )
29 10 28 eqeltrid 
 |-  ( ph -> ( x e. ( M [,] N ) |-> -u A ) e. ( ( M [,] N ) -cn-> RR ) )
30 negex 
 |-  -u B e. _V
31 30 a1i 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> -u B e. _V )
32 reelprrecn 
 |-  RR e. { RR , CC }
33 32 a1i 
 |-  ( ph -> RR e. { RR , CC } )
34 ioossicc 
 |-  ( M (,) N ) C_ ( M [,] N )
35 34 sseli 
 |-  ( x e. ( M (,) N ) -> x e. ( M [,] N ) )
36 cncff 
 |-  ( ( x e. ( M [,] N ) |-> A ) e. ( ( M [,] N ) -cn-> RR ) -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
37 2 36 syl 
 |-  ( ph -> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
38 37 fvmptelrn 
 |-  ( ( ph /\ x e. ( M [,] N ) ) -> A e. RR )
39 35 38 sylan2 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> A e. RR )
40 39 recnd 
 |-  ( ( ph /\ x e. ( M (,) N ) ) -> A e. CC )
41 33 40 3 4 dvmptneg 
 |-  ( ph -> ( RR _D ( x e. ( M (,) N ) |-> -u A ) ) = ( x e. ( M (,) N ) |-> -u B ) )
42 5 negeqd 
 |-  ( x = M -> -u A = -u C )
43 6 negeqd 
 |-  ( x = N -> -u A = -u D )
44 7 renegcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> -u X e. RR )
45 16 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR )
46 45 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M e. RR* )
47 elfzole1 
 |-  ( k e. ( M ..^ N ) -> M <_ k )
48 47 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> M <_ k )
49 iooss1 
 |-  ( ( M e. RR* /\ M <_ k ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
50 46 48 49 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) ( k + 1 ) ) )
51 19 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR )
52 51 rexrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> N e. RR* )
53 fzofzp1 
 |-  ( k e. ( M ..^ N ) -> ( k + 1 ) e. ( M ... N ) )
54 53 adantl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) e. ( M ... N ) )
55 elfzle2 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( k + 1 ) <_ N )
56 54 55 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k + 1 ) <_ N )
57 iooss2 
 |-  ( ( N e. RR* /\ ( k + 1 ) <_ N ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
58 52 56 57 syl2anc 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( M (,) ( k + 1 ) ) C_ ( M (,) N ) )
59 50 58 sstrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( k (,) ( k + 1 ) ) C_ ( M (,) N ) )
60 59 sselda 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> x e. ( M (,) N ) )
61 38 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M [,] N ) ) -> A e. RR )
62 35 61 sylan2 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> A e. RR )
63 62 fmpttd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> A ) : ( M (,) N ) --> RR )
64 ioossre 
 |-  ( M (,) N ) C_ RR
65 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 )
66 63 64 65 sylancl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) : dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) --> RR )
67 4 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( x e. ( M (,) N ) |-> B ) )
68 67 dmeqd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = dom ( x e. ( M (,) N ) |-> B ) )
69 3 adantlr 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> B e. V )
70 69 ralrimiva 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A. x e. ( M (,) N ) B e. V )
71 dmmptg 
 |-  ( A. x e. ( M (,) N ) B e. V -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
72 70 71 syl 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( x e. ( M (,) N ) |-> B ) = ( M (,) N ) )
73 68 72 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> dom ( RR _D ( x e. ( M (,) N ) |-> A ) ) = ( M (,) N ) )
74 67 73 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 ) )
75 66 74 mpbid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( x e. ( M (,) N ) |-> B ) : ( M (,) N ) --> RR )
76 75 fvmptelrn 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( M (,) N ) ) -> B e. RR )
77 60 76 syldan 
 |-  ( ( ( ph /\ k e. ( M ..^ N ) ) /\ x e. ( k (,) ( k + 1 ) ) ) -> B e. RR )
78 77 anasss 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> B e. RR )
79 7 adantrr 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> X e. RR )
80 78 79 lenegd 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> ( B <_ X <-> -u X <_ -u B ) )
81 8 80 mpbid 
 |-  ( ( ph /\ ( k e. ( M ..^ N ) /\ x e. ( k (,) ( k + 1 ) ) ) ) -> -u X <_ -u B )
82 1 29 31 41 42 43 44 81 dvfsumle 
 |-  ( ph -> sum_ k e. ( M ..^ N ) -u X <_ ( -u D - -u C ) )
83 fzofi 
 |-  ( M ..^ N ) e. Fin
84 83 a1i 
 |-  ( ph -> ( M ..^ N ) e. Fin )
85 7 recnd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> X e. CC )
86 84 85 fsumneg 
 |-  ( ph -> sum_ k e. ( M ..^ N ) -u X = -u sum_ k e. ( M ..^ N ) X )
87 6 eleq1d 
 |-  ( x = N -> ( A e. RR <-> D e. RR ) )
88 eqid 
 |-  ( x e. ( M [,] N ) |-> A ) = ( x e. ( M [,] N ) |-> A )
89 88 fmpt 
 |-  ( A. x e. ( M [,] N ) A e. RR <-> ( x e. ( M [,] N ) |-> A ) : ( M [,] N ) --> RR )
90 37 89 sylibr 
 |-  ( ph -> A. x e. ( M [,] N ) A e. RR )
91 16 rexrd 
 |-  ( ph -> M e. RR* )
92 19 rexrd 
 |-  ( ph -> N e. RR* )
93 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
94 1 93 syl 
 |-  ( ph -> M <_ N )
95 ubicc2 
 |-  ( ( M e. RR* /\ N e. RR* /\ M <_ N ) -> N e. ( M [,] N ) )
96 91 92 94 95 syl3anc 
 |-  ( ph -> N e. ( M [,] N ) )
97 87 90 96 rspcdva 
 |-  ( ph -> D e. RR )
98 97 recnd 
 |-  ( ph -> D e. CC )
99 5 eleq1d 
 |-  ( x = M -> ( A e. RR <-> C e. RR ) )
100 lbicc2 
 |-  ( ( M e. RR* /\ N e. RR* /\ M <_ N ) -> M e. ( M [,] N ) )
101 91 92 94 100 syl3anc 
 |-  ( ph -> M e. ( M [,] N ) )
102 99 90 101 rspcdva 
 |-  ( ph -> C e. RR )
103 102 recnd 
 |-  ( ph -> C e. CC )
104 98 103 neg2subd 
 |-  ( ph -> ( -u D - -u C ) = ( C - D ) )
105 98 103 negsubdi2d 
 |-  ( ph -> -u ( D - C ) = ( C - D ) )
106 104 105 eqtr4d 
 |-  ( ph -> ( -u D - -u C ) = -u ( D - C ) )
107 82 86 106 3brtr3d 
 |-  ( ph -> -u sum_ k e. ( M ..^ N ) X <_ -u ( D - C ) )
108 97 102 resubcld 
 |-  ( ph -> ( D - C ) e. RR )
109 84 7 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ..^ N ) X e. RR )
110 108 109 lenegd 
 |-  ( ph -> ( ( D - C ) <_ sum_ k e. ( M ..^ N ) X <-> -u sum_ k e. ( M ..^ N ) X <_ -u ( D - C ) ) )
111 107 110 mpbird 
 |-  ( ph -> ( D - C ) <_ sum_ k e. ( M ..^ N ) X )