Metamath Proof Explorer


Theorem esummono

Description: Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017)

Ref Expression
Hypotheses esummono.f kφ
esummono.c φCV
esummono.b φkCB0+∞
esummono.a φAC
Assertion esummono φ*kAB*kCB

Proof

Step Hyp Ref Expression
1 esummono.f kφ
2 esummono.c φCV
3 esummono.b φkCB0+∞
4 esummono.a φAC
5 2 difexd φCAV
6 simpr φkCAkCA
7 6 eldifad φkCAkC
8 7 3 syldan φkCAB0+∞
9 8 ex φkCAB0+∞
10 1 9 ralrimi φkCAB0+∞
11 nfcv _kCA
12 11 esumcl CAVkCAB0+∞*kCAB0+∞
13 5 10 12 syl2anc φ*kCAB0+∞
14 elxrge0 *kCAB0+∞*kCAB*0*kCAB
15 14 simprbi *kCAB0+∞0*kCAB
16 13 15 syl φ0*kCAB
17 iccssxr 0+∞*
18 2 4 ssexd φAV
19 4 sselda φkAkC
20 19 3 syldan φkAB0+∞
21 20 ex φkAB0+∞
22 1 21 ralrimi φkAB0+∞
23 nfcv _kA
24 23 esumcl AVkAB0+∞*kAB0+∞
25 18 22 24 syl2anc φ*kAB0+∞
26 17 25 sselid φ*kAB*
27 17 13 sselid φ*kCAB*
28 xraddge02 *kAB**kCAB*0*kCAB*kAB*kAB+𝑒*kCAB
29 26 27 28 syl2anc φ0*kCAB*kAB*kAB+𝑒*kCAB
30 16 29 mpd φ*kAB*kAB+𝑒*kCAB
31 disjdif ACA=
32 31 a1i φACA=
33 1 23 11 18 5 32 20 8 esumsplit φ*kACAB=*kAB+𝑒*kCAB
34 undif ACACA=C
35 4 34 sylib φACA=C
36 1 35 esumeq1d φ*kACAB=*kCB
37 33 36 eqtr3d φ*kAB+𝑒*kCAB=*kCB
38 30 37 breqtrd φ*kAB*kCB