Metamath Proof Explorer

Theorem sge0split

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0split.a ⊢φ→A∈V
sge0split.b ⊢φ→B∈W
sge0split.u ⊢U=A∪B
sge0split.in0 ⊢φ→A∩B=∅
sge0split.f ⊢φ→F:U⟶0+∞
Assertion sge0split ⊢φ→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B

Proof

Step Hyp Ref Expression
1 sge0split.a ⊢φ→A∈V
2 sge0split.b ⊢φ→B∈W
3 sge0split.u ⊢U=A∪B
4 sge0split.in0 ⊢φ→A∩B=∅
5 sge0split.f ⊢φ→F:U⟶0+∞
6 1 adantr ⊢φ∧sum^⁡F∈ℝ→A∈V
7 2 adantr ⊢φ∧sum^⁡F∈ℝ→B∈W
8 4 adantr ⊢φ∧sum^⁡F∈ℝ→A∩B=∅
9 5 adantr ⊢φ∧sum^⁡F∈ℝ→F:U⟶0+∞
10 simpr ⊢φ∧sum^⁡F∈ℝ→sum^⁡F∈ℝ
11 6 7 3 8 9 10 sge0resplit ⊢φ∧sum^⁡F∈ℝ→sum^⁡F=sum^⁡F↾A+sum^⁡F↾B
12 unexg ⊢A∈V∧B∈W→A∪B∈V
13 1 2 12 syl2anc ⊢φ→A∪B∈V
14 3 13 eqeltrid ⊢φ→U∈V
15 14 adantr ⊢φ∧sum^⁡F∈ℝ→U∈V
16 15 9 10 sge0ssre ⊢φ∧sum^⁡F∈ℝ→sum^⁡F↾A∈ℝ
17 15 9 10 sge0ssre ⊢φ∧sum^⁡F∈ℝ→sum^⁡F↾B∈ℝ
18 rexadd ⊢sum^⁡F↾A∈ℝ∧sum^⁡F↾B∈ℝ→sum^⁡F↾A+𝑒sum^⁡F↾B=sum^⁡F↾A+sum^⁡F↾B
19 16 17 18 syl2anc ⊢φ∧sum^⁡F∈ℝ→sum^⁡F↾A+𝑒sum^⁡F↾B=sum^⁡F↾A+sum^⁡F↾B
20 19 eqcomd ⊢φ∧sum^⁡F∈ℝ→sum^⁡F↾A+sum^⁡F↾B=sum^⁡F↾A+𝑒sum^⁡F↾B
21 11 20 eqtrd ⊢φ∧sum^⁡F∈ℝ→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B
22 simpl ⊢φ∧¬sum^⁡F∈ℝ→φ
23 simpr ⊢φ∧¬sum^⁡F∈ℝ→¬sum^⁡F∈ℝ
24 14 5 sge0repnf ⊢φ→sum^⁡F∈ℝ↔¬sum^⁡F=+∞
25 24 adantr ⊢φ∧¬sum^⁡F∈ℝ→sum^⁡F∈ℝ↔¬sum^⁡F=+∞
26 23 25 mtbid ⊢φ∧¬sum^⁡F∈ℝ→¬¬sum^⁡F=+∞
27 26 notnotrd ⊢φ∧¬sum^⁡F∈ℝ→sum^⁡F=+∞
28 14 5 sge0xrcl ⊢φ→sum^⁡F∈ℝ*
29 28 adantr ⊢φ∧sum^⁡F=+∞→sum^⁡F∈ℝ*
30 ssun1 ⊢A⊆A∪B
31 30 3 sseqtrri ⊢A⊆U
32 31 a1i ⊢φ→A⊆U
33 5 32 fssresd ⊢φ→F↾A:A⟶0+∞
34 1 33 sge0xrcl ⊢φ→sum^⁡F↾A∈ℝ*
35 iccssxr ⊢0+∞⊆ℝ*
36 ssun2 ⊢B⊆A∪B
37 36 3 sseqtrri ⊢B⊆U
38 37 a1i ⊢φ→B⊆U
39 5 38 fssresd ⊢φ→F↾B:B⟶0+∞
40 2 39 sge0cl ⊢φ→sum^⁡F↾B∈0+∞
41 35 40 sselid ⊢φ→sum^⁡F↾B∈ℝ*
42 34 41 xaddcld ⊢φ→sum^⁡F↾A+𝑒sum^⁡F↾B∈ℝ*
43 42 adantr ⊢φ∧sum^⁡F=+∞→sum^⁡F↾A+𝑒sum^⁡F↾B∈ℝ*
44 pnfxr ⊢+∞∈ℝ*
45 eqid ⊢+∞=+∞
46 xreqle ⊢+∞∈ℝ*∧+∞=+∞→+∞≤+∞
47 44 45 46 mp2an ⊢+∞≤+∞
48 47 a1i ⊢φ∧+∞∈ran⁡F↾A→+∞≤+∞
49 14 adantr ⊢φ∧+∞∈ran⁡F↾A→U∈V
50 5 adantr ⊢φ∧+∞∈ran⁡F↾A→F:U⟶0+∞
51 rnresss ⊢ran⁡F↾A⊆ran⁡F
52 51 sseli ⊢+∞∈ran⁡F↾A→+∞∈ran⁡F
53 52 adantl ⊢φ∧+∞∈ran⁡F↾A→+∞∈ran⁡F
54 49 50 53 sge0pnfval ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F=+∞
55 xrge0neqmnf ⊢sum^⁡F↾B∈0+∞→sum^⁡F↾B≠−∞
56 40 55 syl ⊢φ→sum^⁡F↾B≠−∞
57 xaddpnf2 ⊢sum^⁡F↾B∈ℝ*∧sum^⁡F↾B≠−∞→+∞+𝑒sum^⁡F↾B=+∞
58 41 56 57 syl2anc ⊢φ→+∞+𝑒sum^⁡F↾B=+∞
59 58 eqcomd ⊢φ→+∞=+∞+𝑒sum^⁡F↾B
60 59 adantr ⊢φ∧+∞∈ran⁡F↾A→+∞=+∞+𝑒sum^⁡F↾B
61 1 adantr ⊢φ∧+∞∈ran⁡F↾A→A∈V
62 33 adantr ⊢φ∧+∞∈ran⁡F↾A→F↾A:A⟶0+∞
63 simpr ⊢φ∧+∞∈ran⁡F↾A→+∞∈ran⁡F↾A
64 61 62 63 sge0pnfval ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F↾A=+∞
65 64 oveq1d ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F↾A+𝑒sum^⁡F↾B=+∞+𝑒sum^⁡F↾B
66 60 54 65 3eqtr4d ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B
67 66 54 eqtr3d ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F↾A+𝑒sum^⁡F↾B=+∞
68 54 67 breq12d ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B↔+∞≤+∞
69 48 68 mpbird ⊢φ∧+∞∈ran⁡F↾A→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
70 47 a1i ⊢φ∧+∞∈ran⁡F↾B→+∞≤+∞
71 14 adantr ⊢φ∧+∞∈ran⁡F↾B→U∈V
72 5 adantr ⊢φ∧+∞∈ran⁡F↾B→F:U⟶0+∞
73 rnresss ⊢ran⁡F↾B⊆ran⁡F
74 73 sseli ⊢+∞∈ran⁡F↾B→+∞∈ran⁡F
75 74 adantl ⊢φ∧+∞∈ran⁡F↾B→+∞∈ran⁡F
76 71 72 75 sge0pnfval ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F=+∞
77 2 adantr ⊢φ∧+∞∈ran⁡F↾B→B∈W
78 39 adantr ⊢φ∧+∞∈ran⁡F↾B→F↾B:B⟶0+∞
79 simpr ⊢φ∧+∞∈ran⁡F↾B→+∞∈ran⁡F↾B
80 77 78 79 sge0pnfval ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F↾B=+∞
81 80 oveq2d ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F↾A+𝑒sum^⁡F↾B=sum^⁡F↾A+𝑒+∞
82 1 33 sge0cl ⊢φ→sum^⁡F↾A∈0+∞
83 xrge0neqmnf ⊢sum^⁡F↾A∈0+∞→sum^⁡F↾A≠−∞
84 82 83 syl ⊢φ→sum^⁡F↾A≠−∞
85 xaddpnf1 ⊢sum^⁡F↾A∈ℝ*∧sum^⁡F↾A≠−∞→sum^⁡F↾A+𝑒+∞=+∞
86 34 84 85 syl2anc ⊢φ→sum^⁡F↾A+𝑒+∞=+∞
87 86 adantr ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F↾A+𝑒+∞=+∞
88 81 87 eqtrd ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F↾A+𝑒sum^⁡F↾B=+∞
89 76 88 breq12d ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B↔+∞≤+∞
90 70 89 mpbird ⊢φ∧+∞∈ran⁡F↾B→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
91 90 adantlr ⊢φ∧¬+∞∈ran⁡F↾A∧+∞∈ran⁡F↾B→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
92 simpr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y→z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y
93 vex ⊢z∈V
94 eqid ⊢x∈𝒫U∩Fin⟼∑y∈xF⁡y=x∈𝒫U∩Fin⟼∑y∈xF⁡y
95 94 elrnmpt ⊢z∈V→z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y↔∃x∈𝒫U∩Finz=∑y∈xF⁡y
96 93 95 ax-mp ⊢z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y↔∃x∈𝒫U∩Finz=∑y∈xF⁡y
97 92 96 sylib ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y→∃x∈𝒫U∩Finz=∑y∈xF⁡y
98 simp3 ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧z=∑y∈xF⁡y→z=∑y∈xF⁡y
99 inss1 ⊢x∩A∩x∩B⊆x∩A
100 inss2 ⊢x∩A⊆A
101 99 100 sstri ⊢x∩A∩x∩B⊆A
102 inss2 ⊢x∩A∩x∩B⊆x∩B
103 inss2 ⊢x∩B⊆B
104 102 103 sstri ⊢x∩A∩x∩B⊆B
105 101 104 ssini ⊢x∩A∩x∩B⊆A∩B
106 105 a1i ⊢φ→x∩A∩x∩B⊆A∩B
107 106 4 sseqtrd ⊢φ→x∩A∩x∩B⊆∅
108 ss0 ⊢x∩A∩x∩B⊆∅→x∩A∩x∩B=∅
109 107 108 syl ⊢φ→x∩A∩x∩B=∅
110 109 ad3antrrr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∩A∩x∩B=∅
111 indi ⊢x∩A∪B=x∩A∪x∩B
112 111 eqcomi ⊢x∩A∪x∩B=x∩A∪B
113 112 a1i ⊢x∈𝒫U∩Fin→x∩A∪x∩B=x∩A∪B
114 3 eqcomi ⊢A∪B=U
115 114 ineq2i ⊢x∩A∪B=x∩U
116 115 a1i ⊢x∈𝒫U∩Fin→x∩A∪B=x∩U
117 elinel1 ⊢x∈𝒫U∩Fin→x∈𝒫U
118 elpwi ⊢x∈𝒫U→x⊆U
119 117 118 syl ⊢x∈𝒫U∩Fin→x⊆U
120 df-ss ⊢x⊆U↔x∩U=x
121 120 biimpi ⊢x⊆U→x∩U=x
122 119 121 syl ⊢x∈𝒫U∩Fin→x∩U=x
123 113 116 122 3eqtrrd ⊢x∈𝒫U∩Fin→x=x∩A∪x∩B
124 123 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x=x∩A∪x∩B
125 elinel2 ⊢x∈𝒫U∩Fin→x∈Fin
126 125 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∈Fin
127 rge0ssre ⊢0+∞⊆ℝ
128 5 ad2antrr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→F:U⟶0+∞
129 pm4.56 ⊢¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B↔¬+∞∈ran⁡F↾A∨+∞∈ran⁡F↾B
130 129 biimpi ⊢¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→¬+∞∈ran⁡F↾A∨+∞∈ran⁡F↾B
131 elun ⊢+∞∈ran⁡F↾A∪ran⁡F↾B↔+∞∈ran⁡F↾A∨+∞∈ran⁡F↾B
132 130 131 sylnibr ⊢¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→¬+∞∈ran⁡F↾A∪ran⁡F↾B
133 132 adantll ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→¬+∞∈ran⁡F↾A∪ran⁡F↾B
134 rnresun ⊢ran⁡F↾A∪B=ran⁡F↾A∪ran⁡F↾B
135 134 eqcomi ⊢ran⁡F↾A∪ran⁡F↾B=ran⁡F↾A∪B
136 135 a1i ⊢φ→ran⁡F↾A∪ran⁡F↾B=ran⁡F↾A∪B
137 114 reseq2i ⊢F↾A∪B=F↾U
138 137 rneqi ⊢ran⁡F↾A∪B=ran⁡F↾U
139 138 a1i ⊢φ→ran⁡F↾A∪B=ran⁡F↾U
140 ffn ⊢F:U⟶0+∞→FFnU
141 fnresdm ⊢FFnU→F↾U=F
142 5 140 141 3syl ⊢φ→F↾U=F
143 142 rneqd ⊢φ→ran⁡F↾U=ran⁡F
144 136 139 143 3eqtrd ⊢φ→ran⁡F↾A∪ran⁡F↾B=ran⁡F
145 144 ad2antrr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→ran⁡F↾A∪ran⁡F↾B=ran⁡F
146 133 145 neleqtrd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→¬+∞∈ran⁡F
147 128 146 fge0iccico ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→F:U⟶0+∞
148 147 ad2antrr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x→F:U⟶0+∞
149 119 adantr ⊢x∈𝒫U∩Fin∧y∈x→x⊆U
150 simpr ⊢x∈𝒫U∩Fin∧y∈x→y∈x
151 149 150 sseldd ⊢x∈𝒫U∩Fin∧y∈x→y∈U
152 151 adantll ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x→y∈U
153 148 152 ffvelcdmd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x→F⁡y∈0+∞
154 127 153 sselid ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x→F⁡y∈ℝ
155 154 recnd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x→F⁡y∈ℂ
156 110 124 126 155 fsumsplit ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈xF⁡y=∑y∈x∩AF⁡y+∑y∈x∩BF⁡y
157 infi ⊢x∈Fin→x∩A∈Fin
158 125 157 syl ⊢x∈𝒫U∩Fin→x∩A∈Fin
159 158 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∩A∈Fin
160 simpl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩A→φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin
161 elinel1 ⊢y∈x∩A→y∈x
162 161 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩A→y∈x
163 160 162 154 syl2anc ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩A→F⁡y∈ℝ
164 159 163 fsumrecl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y∈ℝ
165 infi ⊢x∈Fin→x∩B∈Fin
166 125 165 syl ⊢x∈𝒫U∩Fin→x∩B∈Fin
167 166 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∩B∈Fin
168 simpl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩B→φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin
169 elinel1 ⊢y∈x∩B→y∈x
170 169 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩B→y∈x
171 168 170 154 syl2anc ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩B→F⁡y∈ℝ
172 167 171 fsumrecl ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF⁡y∈ℝ
173 rexadd ⊢∑y∈x∩AF⁡y∈ℝ∧∑y∈x∩BF⁡y∈ℝ→∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y=∑y∈x∩AF⁡y+∑y∈x∩BF⁡y
174 164 172 173 syl2anc ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y=∑y∈x∩AF⁡y+∑y∈x∩BF⁡y
175 174 eqcomd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y+∑y∈x∩BF⁡y=∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y
176 156 175 eqtrd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈xF⁡y=∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y
177 ressxr ⊢ℝ⊆ℝ*
178 177 164 sselid ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y∈ℝ*
179 177 172 sselid ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF⁡y∈ℝ*
180 1 adantr ⊢φ∧¬+∞∈ran⁡F↾A→A∈V
181 33 adantr ⊢φ∧¬+∞∈ran⁡F↾A→F↾A:A⟶0+∞
182 simpr ⊢φ∧¬+∞∈ran⁡F↾A→¬+∞∈ran⁡F↾A
183 181 182 fge0iccico ⊢φ∧¬+∞∈ran⁡F↾A→F↾A:A⟶0+∞
184 180 183 sge0reval ⊢φ∧¬+∞∈ran⁡F↾A→sum^⁡F↾A=supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
185 184 eqcomd ⊢φ∧¬+∞∈ran⁡F↾A→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<=sum^⁡F↾A
186 34 adantr ⊢φ∧¬+∞∈ran⁡F↾A→sum^⁡F↾A∈ℝ*
187 185 186 eqeltrd ⊢φ∧¬+∞∈ran⁡F↾A→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*
188 187 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*
189 2 adantr ⊢φ∧¬+∞∈ran⁡F↾B→B∈W
190 39 adantr ⊢φ∧¬+∞∈ran⁡F↾B→F↾B:B⟶0+∞
191 simpr ⊢φ∧¬+∞∈ran⁡F↾B→¬+∞∈ran⁡F↾B
192 190 191 fge0iccico ⊢φ∧¬+∞∈ran⁡F↾B→F↾B:B⟶0+∞
193 189 192 sge0reval ⊢φ∧¬+∞∈ran⁡F↾B→sum^⁡F↾B=supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
194 193 eqcomd ⊢φ∧¬+∞∈ran⁡F↾B→supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<=sum^⁡F↾B
195 41 adantr ⊢φ∧¬+∞∈ran⁡F↾B→sum^⁡F↾B∈ℝ*
196 194 195 eqeltrd ⊢φ∧¬+∞∈ran⁡F↾B→supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
197 196 adantlr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
198 188 197 jca ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*∧supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
199 198 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*∧supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
200 178 179 199 jca31 ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y∈ℝ*∧∑y∈x∩BF⁡y∈ℝ*∧supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*∧supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
201 180 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→A∈V
202 181 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→F↾A:A⟶0+∞
203 182 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→¬+∞∈ran⁡F↾A
204 202 203 fge0iccico ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→F↾A:A⟶0+∞
205 100 a1i ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→x∩A⊆A
206 158 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→x∩A∈Fin
207 201 204 205 206 fsumlesge0 ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→∑y∈x∩AF↾A⁡y≤sum^⁡F↾A
208 100 sseli ⊢y∈x∩A→y∈A
209 fvres ⊢y∈A→F↾A⁡y=F⁡y
210 208 209 syl ⊢y∈x∩A→F↾A⁡y=F⁡y
211 210 adantl ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin∧y∈x∩A→F↾A⁡y=F⁡y
212 211 sumeq2dv ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→∑y∈x∩AF↾A⁡y=∑y∈x∩AF⁡y
213 184 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→sum^⁡F↾A=supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
214 212 213 breq12d ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→∑y∈x∩AF↾A⁡y≤sum^⁡F↾A↔∑y∈x∩AF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
215 207 214 mpbid ⊢φ∧¬+∞∈ran⁡F↾A∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
216 215 adantlr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
217 189 adantr ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→B∈W
218 190 adantr ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→F↾B:B⟶0+∞
219 191 adantr ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→¬+∞∈ran⁡F↾B
220 218 219 fge0iccico ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→F↾B:B⟶0+∞
221 103 a1i ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∩B⊆B
222 166 adantl ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→x∩B∈Fin
223 217 220 221 222 fsumlesge0 ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF↾B⁡y≤sum^⁡F↾B
224 103 sseli ⊢y∈x∩B→y∈B
225 fvres ⊢y∈B→F↾B⁡y=F⁡y
226 224 225 syl ⊢y∈x∩B→F↾B⁡y=F⁡y
227 226 adantl ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧y∈x∩B→F↾B⁡y=F⁡y
228 227 sumeq2dv ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF↾B⁡y=∑y∈x∩BF⁡y
229 193 adantr ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→sum^⁡F↾B=supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
230 228 229 breq12d ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF↾B⁡y≤sum^⁡F↾B↔∑y∈x∩BF⁡y≤supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
231 223 230 mpbid ⊢φ∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF⁡y≤supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
232 231 adantllr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩BF⁡y≤supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
233 216 232 jca ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∧∑y∈x∩BF⁡y≤supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
234 xle2add ⊢∑y∈x∩AF⁡y∈ℝ*∧∑y∈x∩BF⁡y∈ℝ*∧supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∈ℝ*∧supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*→∑y∈x∩AF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<∧∑y∈x∩BF⁡y≤supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<→∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
235 200 233 234 sylc ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈x∩AF⁡y+𝑒∑y∈x∩BF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
236 176 235 eqbrtrd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin→∑y∈xF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
237 236 3adant3 ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧z=∑y∈xF⁡y→∑y∈xF⁡y≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
238 98 237 eqbrtrd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧x∈𝒫U∩Fin∧z=∑y∈xF⁡y→z≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
239 238 3exp ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→x∈𝒫U∩Fin→z=∑y∈xF⁡y→z≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
240 239 rexlimdv ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→∃x∈𝒫U∩Finz=∑y∈xF⁡y→z≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
241 240 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y→∃x∈𝒫U∩Finz=∑y∈xF⁡y→z≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
242 97 241 mpd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B∧z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y→z≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
243 242 ralrimiva ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→∀z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yz≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
244 147 sge0rnre ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y⊆ℝ
245 177 a1i ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→ℝ⊆ℝ*
246 244 245 sstrd ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y⊆ℝ*
247 188 197 xaddcld ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*
248 supxrleub ⊢ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡y⊆ℝ*∧supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<∈ℝ*→supran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yℝ*<≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<↔∀z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yz≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
249 246 247 248 syl2anc ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yℝ*<≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<↔∀z∈ran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yz≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
250 243 249 mpbird ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→supran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yℝ*<≤supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
251 14 ad2antrr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→U∈V
252 251 147 sge0reval ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→sum^⁡F=supran⁡x∈𝒫U∩Fin⟼∑y∈xF⁡yℝ*<
253 184 adantr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→sum^⁡F↾A=supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<
254 193 adantlr ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→sum^⁡F↾B=supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
255 253 254 oveq12d ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→sum^⁡F↾A+𝑒sum^⁡F↾B=supran⁡a∈𝒫A∩Fin⟼∑b∈aF↾A⁡bℝ*<+𝑒supran⁡c∈𝒫B∩Fin⟼∑d∈cF↾B⁡dℝ*<
256 250 252 255 3brtr4d ⊢φ∧¬+∞∈ran⁡F↾A∧¬+∞∈ran⁡F↾B→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
257 91 256 pm2.61dan ⊢φ∧¬+∞∈ran⁡F↾A→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
258 69 257 pm2.61dan ⊢φ→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
259 258 adantr ⊢φ∧sum^⁡F=+∞→sum^⁡F≤sum^⁡F↾A+𝑒sum^⁡F↾B
260 pnfge ⊢sum^⁡F↾A+𝑒sum^⁡F↾B∈ℝ*→sum^⁡F↾A+𝑒sum^⁡F↾B≤+∞
261 42 260 syl ⊢φ→sum^⁡F↾A+𝑒sum^⁡F↾B≤+∞
262 261 adantr ⊢φ∧sum^⁡F=+∞→sum^⁡F↾A+𝑒sum^⁡F↾B≤+∞
263 id ⊢sum^⁡F=+∞→sum^⁡F=+∞
264 263 eqcomd ⊢sum^⁡F=+∞→+∞=sum^⁡F
265 264 adantl ⊢φ∧sum^⁡F=+∞→+∞=sum^⁡F
266 262 265 breqtrd ⊢φ∧sum^⁡F=+∞→sum^⁡F↾A+𝑒sum^⁡F↾B≤sum^⁡F
267 29 43 259 266 xrletrid ⊢φ∧sum^⁡F=+∞→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B
268 22 27 267 syl2anc ⊢φ∧¬sum^⁡F∈ℝ→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B
269 21 268 pm2.61dan ⊢φ→sum^⁡F=sum^⁡F↾A+𝑒sum^⁡F↾B