Description: The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | esumpmono.1 | |
|
esumpmono.2 | |
||
esumpmono.3 | |
||
Assertion | esumpmono | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | esumpmono.1 | |
|
2 | esumpmono.2 | |
|
3 | esumpmono.3 | |
|
4 | iccssxr | |
|
5 | ovexd | |
|
6 | elfznn | |
|
7 | icossicc | |
|
8 | 7 3 | sselid | |
9 | 6 8 | sylan2 | |
10 | 9 | ralrimiva | |
11 | nfcv | |
|
12 | 11 | esumcl | |
13 | 5 10 12 | syl2anc | |
14 | 4 13 | sselid | |
15 | 14 | xrleidd | |
16 | ovexd | |
|
17 | 1 | adantr | |
18 | peano2nn | |
|
19 | nnuz | |
|
20 | 18 19 | eleqtrdi | |
21 | fzss1 | |
|
22 | 17 20 21 | 3syl | |
23 | simpr | |
|
24 | 22 23 | sseldd | |
25 | elfznn | |
|
26 | 24 25 | syl | |
27 | 26 8 | syldan | |
28 | 27 | ralrimiva | |
29 | nfcv | |
|
30 | 29 | esumcl | |
31 | 16 28 30 | syl2anc | |
32 | elxrge0 | |
|
33 | 32 | simprbi | |
34 | 31 33 | syl | |
35 | 0xr | |
|
36 | 35 | a1i | |
37 | 4 31 | sselid | |
38 | xle2add | |
|
39 | 14 36 14 37 38 | syl22anc | |
40 | 15 34 39 | mp2and | |
41 | xaddid1 | |
|
42 | 14 41 | syl | |
43 | 42 | eqcomd | |
44 | 1 19 | eleqtrdi | |
45 | eluzfz | |
|
46 | 44 2 45 | syl2anc | |
47 | fzsplit | |
|
48 | esumeq1 | |
|
49 | 46 47 48 | 3syl | |
50 | nfv | |
|
51 | nnre | |
|
52 | 51 | ltp1d | |
53 | fzdisj | |
|
54 | 1 52 53 | 3syl | |
55 | 50 11 29 5 16 54 9 27 | esumsplit | |
56 | 49 55 | eqtrd | |
57 | 40 43 56 | 3brtr4d | |