Metamath Proof Explorer

Theorem esumpmono

Description: The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Hypotheses esumpmono.1 
|- ( ph -> M e. NN )
esumpmono.2 
|- ( ph -> N e. ( ZZ>= ` M ) )
esumpmono.3 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
Assertion esumpmono 
|- ( ph -> sum* k e. ( 1 ... M ) A <_ sum* k e. ( 1 ... N ) A )

Proof

Step Hyp Ref Expression
1 esumpmono.1 
 |-  ( ph -> M e. NN )
2 esumpmono.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 esumpmono.3 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
4 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
5 ovexd 
 |-  ( ph -> ( 1 ... M ) e. _V )
6 elfznn 
 |-  ( k e. ( 1 ... M ) -> k e. NN )
7 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
8 7 3 sselid 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
9 6 8 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> A e. ( 0 [,] +oo ) )
10 9 ralrimiva 
 |-  ( ph -> A. k e. ( 1 ... M ) A e. ( 0 [,] +oo ) )
11 nfcv 
 |-  F/_ k ( 1 ... M )
12 11 esumcl 
 |-  ( ( ( 1 ... M ) e. _V /\ A. k e. ( 1 ... M ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... M ) A e. ( 0 [,] +oo ) )
13 5 10 12 syl2anc 
 |-  ( ph -> sum* k e. ( 1 ... M ) A e. ( 0 [,] +oo ) )
14 4 13 sselid 
 |-  ( ph -> sum* k e. ( 1 ... M ) A e. RR* )
15 14 xrleidd 
 |-  ( ph -> sum* k e. ( 1 ... M ) A <_ sum* k e. ( 1 ... M ) A )
16 ovexd 
 |-  ( ph -> ( ( M + 1 ) ... N ) e. _V )
17 1 adantr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> M e. NN )
18 peano2nn 
 |-  ( M e. NN -> ( M + 1 ) e. NN )
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 18 19 eleqtrdi 
 |-  ( M e. NN -> ( M + 1 ) e. ( ZZ>= ` 1 ) )
21 fzss1 
 |-  ( ( M + 1 ) e. ( ZZ>= ` 1 ) -> ( ( M + 1 ) ... N ) C_ ( 1 ... N ) )
22 17 20 21 3syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> ( ( M + 1 ) ... N ) C_ ( 1 ... N ) )
23 simpr 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> k e. ( ( M + 1 ) ... N ) )
24 22 23 sseldd 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> k e. ( 1 ... N ) )
25 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
26 24 25 syl 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> k e. NN )
27 26 8 syldan 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> A e. ( 0 [,] +oo ) )
28 27 ralrimiva 
 |-  ( ph -> A. k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) )
29 nfcv 
 |-  F/_ k ( ( M + 1 ) ... N )
30 29 esumcl 
 |-  ( ( ( ( M + 1 ) ... N ) e. _V /\ A. k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) )
31 16 28 30 syl2anc 
 |-  ( ph -> sum* k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) )
32 elxrge0 
 |-  ( sum* k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) <-> ( sum* k e. ( ( M + 1 ) ... N ) A e. RR* /\ 0 <_ sum* k e. ( ( M + 1 ) ... N ) A ) )
33 32 simprbi 
 |-  ( sum* k e. ( ( M + 1 ) ... N ) A e. ( 0 [,] +oo ) -> 0 <_ sum* k e. ( ( M + 1 ) ... N ) A )
34 31 33 syl 
 |-  ( ph -> 0 <_ sum* k e. ( ( M + 1 ) ... N ) A )
35 0xr 
 |-  0 e. RR*
36 35 a1i 
 |-  ( ph -> 0 e. RR* )
37 4 31 sselid 
 |-  ( ph -> sum* k e. ( ( M + 1 ) ... N ) A e. RR* )
38 xle2add 
 |-  ( ( ( sum* k e. ( 1 ... M ) A e. RR* /\ 0 e. RR* ) /\ ( sum* k e. ( 1 ... M ) A e. RR* /\ sum* k e. ( ( M + 1 ) ... N ) A e. RR* ) ) -> ( ( sum* k e. ( 1 ... M ) A <_ sum* k e. ( 1 ... M ) A /\ 0 <_ sum* k e. ( ( M + 1 ) ... N ) A ) -> ( sum* k e. ( 1 ... M ) A +e 0 ) <_ ( sum* k e. ( 1 ... M ) A +e sum* k e. ( ( M + 1 ) ... N ) A ) ) )
39 14 36 14 37 38 syl22anc 
 |-  ( ph -> ( ( sum* k e. ( 1 ... M ) A <_ sum* k e. ( 1 ... M ) A /\ 0 <_ sum* k e. ( ( M + 1 ) ... N ) A ) -> ( sum* k e. ( 1 ... M ) A +e 0 ) <_ ( sum* k e. ( 1 ... M ) A +e sum* k e. ( ( M + 1 ) ... N ) A ) ) )
40 15 34 39 mp2and 
 |-  ( ph -> ( sum* k e. ( 1 ... M ) A +e 0 ) <_ ( sum* k e. ( 1 ... M ) A +e sum* k e. ( ( M + 1 ) ... N ) A ) )
41 xaddrid 
 |-  ( sum* k e. ( 1 ... M ) A e. RR* -> ( sum* k e. ( 1 ... M ) A +e 0 ) = sum* k e. ( 1 ... M ) A )
42 14 41 syl 
 |-  ( ph -> ( sum* k e. ( 1 ... M ) A +e 0 ) = sum* k e. ( 1 ... M ) A )
43 42 eqcomd 
 |-  ( ph -> sum* k e. ( 1 ... M ) A = ( sum* k e. ( 1 ... M ) A +e 0 ) )
44 1 19 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
45 eluzfz 
 |-  ( ( M e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` M ) ) -> M e. ( 1 ... N ) )
46 44 2 45 syl2anc 
 |-  ( ph -> M e. ( 1 ... N ) )
47 fzsplit 
 |-  ( M e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) )
48 esumeq1 
 |-  ( ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) -> sum* k e. ( 1 ... N ) A = sum* k e. ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) A )
49 46 47 48 3syl 
 |-  ( ph -> sum* k e. ( 1 ... N ) A = sum* k e. ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) A )
50 nfv 
 |-  F/ k ph
51 nnre 
 |-  ( M e. NN -> M e. RR )
52 51 ltp1d 
 |-  ( M e. NN -> M < ( M + 1 ) )
53 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
54 1 52 53 3syl 
 |-  ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
55 50 11 29 5 16 54 9 27 esumsplit 
 |-  ( ph -> sum* k e. ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) A = ( sum* k e. ( 1 ... M ) A +e sum* k e. ( ( M + 1 ) ... N ) A ) )
56 49 55 eqtrd 
 |-  ( ph -> sum* k e. ( 1 ... N ) A = ( sum* k e. ( 1 ... M ) A +e sum* k e. ( ( M + 1 ) ... N ) A ) )
57 40 43 56 3brtr4d 
 |-  ( ph -> sum* k e. ( 1 ... M ) A <_ sum* k e. ( 1 ... N ) A )