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 φM
esumpmono.2 φNM
esumpmono.3 φkA0+∞
Assertion esumpmono φ*k=1MA*k=1NA

Proof

Step Hyp Ref Expression
1 esumpmono.1 φM
2 esumpmono.2 φNM
3 esumpmono.3 φkA0+∞
4 iccssxr 0+∞*
5 ovexd φ1MV
6 elfznn k1Mk
7 icossicc 0+∞0+∞
8 7 3 sselid φkA0+∞
9 6 8 sylan2 φk1MA0+∞
10 9 ralrimiva φk1MA0+∞
11 nfcv _k1M
12 11 esumcl 1MVk1MA0+∞*k=1MA0+∞
13 5 10 12 syl2anc φ*k=1MA0+∞
14 4 13 sselid φ*k=1MA*
15 14 xrleidd φ*k=1MA*k=1MA
16 ovexd φM+1NV
17 1 adantr φkM+1NM
18 peano2nn MM+1
19 nnuz =1
20 18 19 eleqtrdi MM+11
21 fzss1 M+11M+1N1N
22 17 20 21 3syl φkM+1NM+1N1N
23 simpr φkM+1NkM+1N
24 22 23 sseldd φkM+1Nk1N
25 elfznn k1Nk
26 24 25 syl φkM+1Nk
27 26 8 syldan φkM+1NA0+∞
28 27 ralrimiva φkM+1NA0+∞
29 nfcv _kM+1N
30 29 esumcl M+1NVkM+1NA0+∞*k=M+1NA0+∞
31 16 28 30 syl2anc φ*k=M+1NA0+∞
32 elxrge0 *k=M+1NA0+∞*k=M+1NA*0*k=M+1NA
33 32 simprbi *k=M+1NA0+∞0*k=M+1NA
34 31 33 syl φ0*k=M+1NA
35 0xr 0*
36 35 a1i φ0*
37 4 31 sselid φ*k=M+1NA*
38 xle2add *k=1MA*0**k=1MA**k=M+1NA**k=1MA*k=1MA0*k=M+1NA*k=1MA+𝑒0*k=1MA+𝑒*k=M+1NA
39 14 36 14 37 38 syl22anc φ*k=1MA*k=1MA0*k=M+1NA*k=1MA+𝑒0*k=1MA+𝑒*k=M+1NA
40 15 34 39 mp2and φ*k=1MA+𝑒0*k=1MA+𝑒*k=M+1NA
41 xaddid1 *k=1MA**k=1MA+𝑒0=*k=1MA
42 14 41 syl φ*k=1MA+𝑒0=*k=1MA
43 42 eqcomd φ*k=1MA=*k=1MA+𝑒0
44 1 19 eleqtrdi φM1
45 eluzfz M1NMM1N
46 44 2 45 syl2anc φM1N
47 fzsplit M1N1N=1MM+1N
48 esumeq1 1N=1MM+1N*k=1NA=*k1MM+1NA
49 46 47 48 3syl φ*k=1NA=*k1MM+1NA
50 nfv kφ
51 nnre MM
52 51 ltp1d MM<M+1
53 fzdisj M<M+11MM+1N=
54 1 52 53 3syl φ1MM+1N=
55 50 11 29 5 16 54 9 27 esumsplit φ*k1MM+1NA=*k=1MA+𝑒*k=M+1NA
56 49 55 eqtrd φ*k=1NA=*k=1MA+𝑒*k=M+1NA
57 40 43 56 3brtr4d φ*k=1MA*k=1NA