Metamath Proof Explorer


Theorem xrge0gsumle

Description: A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses xrge0gsumle.g G=𝑠*𝑠0+∞
xrge0gsumle.a φAV
xrge0gsumle.f φF:A0+∞
xrge0gsumle.b φB𝒫AFin
xrge0gsumle.c φCB
Assertion xrge0gsumle φGFCGFB

Proof

Step Hyp Ref Expression
1 xrge0gsumle.g G=𝑠*𝑠0+∞
2 xrge0gsumle.a φAV
3 xrge0gsumle.f φF:A0+∞
4 xrge0gsumle.b φB𝒫AFin
5 xrge0gsumle.c φCB
6 iccssxr 0+∞*
7 xrsbas *=Base𝑠*
8 1 7 ressbas2 0+∞*0+∞=BaseG
9 6 8 ax-mp 0+∞=BaseG
10 eqid 𝑠*𝑠*−∞=𝑠*𝑠*−∞
11 10 xrge0subm 0+∞SubMnd𝑠*𝑠*−∞
12 xrex *V
13 12 difexi *−∞V
14 simpl x*0xx*
15 ge0nemnf x*0xx−∞
16 14 15 jca x*0xx*x−∞
17 elxrge0 x0+∞x*0x
18 eldifsn x*−∞x*x−∞
19 16 17 18 3imtr4i x0+∞x*−∞
20 19 ssriv 0+∞*−∞
21 ressabs *−∞V0+∞*−∞𝑠*𝑠*−∞𝑠0+∞=𝑠*𝑠0+∞
22 13 20 21 mp2an 𝑠*𝑠*−∞𝑠0+∞=𝑠*𝑠0+∞
23 1 22 eqtr4i G=𝑠*𝑠*−∞𝑠0+∞
24 10 xrs10 0=0𝑠*𝑠*−∞
25 23 24 subm0 0+∞SubMnd𝑠*𝑠*−∞0=0G
26 11 25 ax-mp 0=0G
27 xrge0cmn 𝑠*𝑠0+∞CMnd
28 1 27 eqeltri GCMnd
29 28 a1i φs𝒫AFinGCMnd
30 elfpw s𝒫AFinsAsFin
31 30 simprbi s𝒫AFinsFin
32 31 adantl φs𝒫AFinsFin
33 30 simplbi s𝒫AFinsA
34 fssres F:A0+∞sAFs:s0+∞
35 3 33 34 syl2an φs𝒫AFinFs:s0+∞
36 c0ex 0V
37 36 a1i φs𝒫AFin0V
38 35 32 37 fdmfifsupp φs𝒫AFinfinSupp0Fs
39 9 26 29 32 35 38 gsumcl φs𝒫AFinGFs0+∞
40 6 39 sselid φs𝒫AFinGFs*
41 40 fmpttd φs𝒫AFinGFs:𝒫AFin*
42 41 frnd φrans𝒫AFinGFs*
43 0ss A
44 0fin Fin
45 elfpw 𝒫AFinAFin
46 43 44 45 mpbir2an 𝒫AFin
47 0cn 0
48 eqid s𝒫AFinGFs=s𝒫AFinGFs
49 reseq2 s=Fs=F
50 res0 F=
51 49 50 eqtrdi s=Fs=
52 51 oveq2d s=GFs=G
53 26 gsum0 G=0
54 52 53 eqtrdi s=GFs=0
55 48 54 elrnmpt1s 𝒫AFin00rans𝒫AFinGFs
56 46 47 55 mp2an 0rans𝒫AFinGFs
57 56 a1i φ0rans𝒫AFinGFs
58 42 57 sseldd φ0*
59 28 a1i φGCMnd
60 4 elin2d φBFin
61 diffi BFinBCFin
62 60 61 syl φBCFin
63 elfpw B𝒫AFinBABFin
64 63 simplbi B𝒫AFinBA
65 4 64 syl φBA
66 65 ssdifssd φBCA
67 3 66 fssresd φFBC:BC0+∞
68 36 a1i φ0V
69 67 62 68 fdmfifsupp φfinSupp0FBC
70 9 26 59 62 67 69 gsumcl φGFBC0+∞
71 6 70 sselid φGFBC*
72 60 5 ssfid φCFin
73 5 65 sstrd φCA
74 3 73 fssresd φFC:C0+∞
75 74 72 68 fdmfifsupp φfinSupp0FC
76 9 26 59 72 74 75 gsumcl φGFC0+∞
77 6 76 sselid φGFC*
78 elxrge0 GFBC0+∞GFBC*0GFBC
79 78 simprbi GFBC0+∞0GFBC
80 70 79 syl φ0GFBC
81 xleadd2a 0*GFBC*GFC*0GFBCGFC+𝑒0GFC+𝑒GFBC
82 58 71 77 80 81 syl31anc φGFC+𝑒0GFC+𝑒GFBC
83 77 xaddid1d φGFC+𝑒0=GFC
84 ovex 0+∞V
85 xrsadd +𝑒=+𝑠*
86 1 85 ressplusg 0+∞V+𝑒=+G
87 84 86 ax-mp +𝑒=+G
88 3 65 fssresd φFB:B0+∞
89 88 60 68 fdmfifsupp φfinSupp0FB
90 disjdif CBC=
91 90 a1i φCBC=
92 undif2 CBC=CB
93 ssequn1 CBCB=B
94 5 93 sylib φCB=B
95 92 94 eqtr2id φB=CBC
96 9 26 87 59 4 88 89 91 95 gsumsplit φGFB=GFBC+𝑒GFBBC
97 5 resabs1d φFBC=FC
98 97 oveq2d φGFBC=GFC
99 difss BCB
100 resabs1 BCBFBBC=FBC
101 99 100 mp1i φFBBC=FBC
102 101 oveq2d φGFBBC=GFBC
103 98 102 oveq12d φGFBC+𝑒GFBBC=GFC+𝑒GFBC
104 96 103 eqtr2d φGFC+𝑒GFBC=GFB
105 82 83 104 3brtr3d φGFCGFB