Description: Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | esummono.f | |
|
esummono.c | |
||
esummono.b | |
||
esummono.a | |
||
Assertion | esummono | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | esummono.f | |
|
2 | esummono.c | |
|
3 | esummono.b | |
|
4 | esummono.a | |
|
5 | 2 | difexd | |
6 | simpr | |
|
7 | 6 | eldifad | |
8 | 7 3 | syldan | |
9 | 8 | ex | |
10 | 1 9 | ralrimi | |
11 | nfcv | |
|
12 | 11 | esumcl | |
13 | 5 10 12 | syl2anc | |
14 | elxrge0 | |
|
15 | 14 | simprbi | |
16 | 13 15 | syl | |
17 | iccssxr | |
|
18 | 2 4 | ssexd | |
19 | 4 | sselda | |
20 | 19 3 | syldan | |
21 | 20 | ex | |
22 | 1 21 | ralrimi | |
23 | nfcv | |
|
24 | 23 | esumcl | |
25 | 18 22 24 | syl2anc | |
26 | 17 25 | sselid | |
27 | 17 13 | sselid | |
28 | xraddge02 | |
|
29 | 26 27 28 | syl2anc | |
30 | 16 29 | mpd | |
31 | disjdif | |
|
32 | 31 | a1i | |
33 | 1 23 11 18 5 32 20 8 | esumsplit | |
34 | undif | |
|
35 | 4 34 | sylib | |
36 | 1 35 | esumeq1d | |
37 | 33 36 | eqtr3d | |
38 | 30 37 | breqtrd | |