Metamath Proof Explorer


Theorem sge0resplit

Description: sum^ splits into two parts, when it's a real number. This is a special case of sge0split . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0resplit.a φAV
sge0resplit.b φBW
sge0resplit.u U=AB
sge0resplit.in0 φAB=
sge0resplit.f φF:U0+∞
sge0resplit.re φsum^F
Assertion sge0resplit φsum^F=sum^FA+sum^FB

Proof

Step Hyp Ref Expression
1 sge0resplit.a φAV
2 sge0resplit.b φBW
3 sge0resplit.u U=AB
4 sge0resplit.in0 φAB=
5 sge0resplit.f φF:U0+∞
6 sge0resplit.re φsum^F
7 ssun1 AAB
8 3 eqcomi AB=U
9 7 8 sseqtri AU
10 9 a1i φAU
11 5 10 fssresd φFA:A0+∞
12 3 a1i φU=AB
13 unexg AVBWABV
14 1 2 13 syl2anc φABV
15 12 14 eqeltrd φUV
16 15 5 6 sge0ssre φsum^FA
17 1 11 16 sge0supre φsum^FA=supranx𝒫AFinyxFAy<
18 17 16 eqeltrrd φsupranx𝒫AFinyxFAy<
19 ssun2 BAB
20 19 8 sseqtri BU
21 20 a1i φBU
22 5 21 fssresd φFB:B0+∞
23 15 5 6 sge0ssre φsum^FB
24 2 22 23 sge0supre φsum^FB=supranx𝒫BFinyxFBy<
25 24 23 eqeltrrd φsupranx𝒫BFinyxFBy<
26 rexadd supranx𝒫AFinyxFAy<supranx𝒫BFinyxFBy<supranx𝒫AFinyxFAy<+𝑒supranx𝒫BFinyxFBy<=supranx𝒫AFinyxFAy<+supranx𝒫BFinyxFBy<
27 18 25 26 syl2anc φsupranx𝒫AFinyxFAy<+𝑒supranx𝒫BFinyxFBy<=supranx𝒫AFinyxFAy<+supranx𝒫BFinyxFBy<
28 15 5 6 sge0rern φ¬+∞ranF
29 nelrnres ¬+∞ranF¬+∞ranFA
30 28 29 syl φ¬+∞ranFA
31 11 30 fge0iccico φFA:A0+∞
32 31 sge0rnre φranx𝒫AFinyxFAy
33 sge0rnn0 ranx𝒫AFinyxFAy
34 33 a1i φranx𝒫AFinyxFAy
35 1 31 sge0reval φsum^FA=supranx𝒫AFinyxFAy*<
36 35 eqcomd φsupranx𝒫AFinyxFAy*<=sum^FA
37 36 16 eqeltrd φsupranx𝒫AFinyxFAy*<
38 supxrre3 ranx𝒫AFinyxFAyranx𝒫AFinyxFAysupranx𝒫AFinyxFAy*<wtranx𝒫AFinyxFAytw
39 32 34 38 syl2anc φsupranx𝒫AFinyxFAy*<wtranx𝒫AFinyxFAytw
40 37 39 mpbid φwtranx𝒫AFinyxFAytw
41 nelrnres ¬+∞ranF¬+∞ranFB
42 28 41 syl φ¬+∞ranFB
43 22 42 fge0iccico φFB:B0+∞
44 43 sge0rnre φranx𝒫BFinyxFBy
45 sge0rnn0 ranx𝒫BFinyxFBy
46 45 a1i φranx𝒫BFinyxFBy
47 2 43 sge0reval φsum^FB=supranx𝒫BFinyxFBy*<
48 47 eqcomd φsupranx𝒫BFinyxFBy*<=sum^FB
49 48 23 eqeltrd φsupranx𝒫BFinyxFBy*<
50 supxrre3 ranx𝒫BFinyxFByranx𝒫BFinyxFBysupranx𝒫BFinyxFBy*<wtranx𝒫BFinyxFBytw
51 44 46 50 syl2anc φsupranx𝒫BFinyxFBy*<wtranx𝒫BFinyxFBytw
52 49 51 mpbid φwtranx𝒫BFinyxFBytw
53 eqid z|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u=z|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u
54 32 34 40 44 46 52 53 supadd φsupranx𝒫AFinyxFAy<+supranx𝒫BFinyxFBy<=supz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u<
55 simpl φrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+uφ
56 vex rV
57 eqeq1 z=rz=v+ur=v+u
58 57 rexbidv z=ruranx𝒫BFinyxFByz=v+uuranx𝒫BFinyxFByr=v+u
59 58 rexbidv z=rvranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+uvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
60 56 59 elab rz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+uvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
61 60 biimpi rz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+uvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
62 61 adantl φrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+uvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
63 simpl φvranx𝒫AFinyxFAyuranx𝒫BFinyxFByφ
64 vex vV
65 sumeq1 x=ayxFAy=yaFAy
66 65 cbvmptv x𝒫AFinyxFAy=a𝒫AFinyaFAy
67 66 elrnmpt vVvranx𝒫AFinyxFAya𝒫AFinv=yaFAy
68 64 67 ax-mp vranx𝒫AFinyxFAya𝒫AFinv=yaFAy
69 68 biimpi vranx𝒫AFinyxFAya𝒫AFinv=yaFAy
70 69 adantr vranx𝒫AFinyxFAyuranx𝒫BFinyxFBya𝒫AFinv=yaFAy
71 vex uV
72 sumeq1 x=byxFBy=ybFBy
73 72 cbvmptv x𝒫BFinyxFBy=b𝒫BFinybFBy
74 73 elrnmpt uVuranx𝒫BFinyxFByb𝒫BFinu=ybFBy
75 71 74 ax-mp uranx𝒫BFinyxFByb𝒫BFinu=ybFBy
76 75 biimpi uranx𝒫BFinyxFByb𝒫BFinu=ybFBy
77 76 adantl vranx𝒫AFinyxFAyuranx𝒫BFinyxFByb𝒫BFinu=ybFBy
78 70 77 jca vranx𝒫AFinyxFAyuranx𝒫BFinyxFBya𝒫AFinv=yaFAyb𝒫BFinu=ybFBy
79 reeanv a𝒫AFinb𝒫BFinv=yaFAyu=ybFBya𝒫AFinv=yaFAyb𝒫BFinu=ybFBy
80 78 79 sylibr vranx𝒫AFinyxFAyuranx𝒫BFinyxFBya𝒫AFinb𝒫BFinv=yaFAyu=ybFBy
81 80 adantl φvranx𝒫AFinyxFAyuranx𝒫BFinyxFBya𝒫AFinb𝒫BFinv=yaFAyu=ybFBy
82 eqid x𝒫UFinyxFy=x𝒫UFinyxFy
83 elinel1 a𝒫AFina𝒫A
84 elpwi a𝒫AaA
85 id aAaA
86 85 9 sstrdi aAaU
87 84 86 syl a𝒫AaU
88 83 87 syl a𝒫AFinaU
89 88 adantr a𝒫AFinb𝒫BFinaU
90 elinel1 b𝒫BFinb𝒫B
91 elpwi b𝒫BbB
92 id bBbB
93 92 20 sstrdi bBbU
94 91 93 syl b𝒫BbU
95 90 94 syl b𝒫BFinbU
96 95 adantl a𝒫AFinb𝒫BFinbU
97 89 96 unssd a𝒫AFinb𝒫BFinabU
98 vex aV
99 vex bV
100 98 99 unex abV
101 100 elpw ab𝒫UabU
102 97 101 sylibr a𝒫AFinb𝒫BFinab𝒫U
103 elinel2 a𝒫AFinaFin
104 103 adantr a𝒫AFinb𝒫BFinaFin
105 elinel2 b𝒫BFinbFin
106 105 adantl a𝒫AFinb𝒫BFinbFin
107 unfi aFinbFinabFin
108 104 106 107 syl2anc a𝒫AFinb𝒫BFinabFin
109 102 108 elind a𝒫AFinb𝒫BFinab𝒫UFin
110 109 adantl φa𝒫AFinb𝒫BFinab𝒫UFin
111 110 ad2antrr φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+uab𝒫UFin
112 simpl v=yaFAyu=ybFByv=yaFAy
113 simpr v=yaFAyu=ybFByu=ybFBy
114 112 113 oveq12d v=yaFAyu=ybFByv+u=yaFAy+ybFBy
115 114 adantl a𝒫AFinb𝒫BFinv=yaFAyu=ybFByv+u=yaFAy+ybFBy
116 83 84 syl a𝒫AFinaA
117 116 sselda a𝒫AFinyayA
118 fvres yAFAy=Fy
119 117 118 syl a𝒫AFinyaFAy=Fy
120 119 sumeq2dv a𝒫AFinyaFAy=yaFy
121 120 adantr a𝒫AFinb𝒫BFinyaFAy=yaFy
122 90 91 syl b𝒫BFinbB
123 122 sselda b𝒫BFinybyB
124 fvres yBFBy=Fy
125 123 124 syl b𝒫BFinybFBy=Fy
126 125 sumeq2dv b𝒫BFinybFBy=ybFy
127 126 adantl a𝒫AFinb𝒫BFinybFBy=ybFy
128 121 127 oveq12d a𝒫AFinb𝒫BFinyaFAy+ybFBy=yaFy+ybFy
129 128 adantr a𝒫AFinb𝒫BFinv=yaFAyu=ybFByyaFAy+ybFBy=yaFy+ybFy
130 115 129 eqtrd a𝒫AFinb𝒫BFinv=yaFAyu=ybFByv+u=yaFy+ybFy
131 130 ad4ant23 φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+uv+u=yaFy+ybFy
132 simpr φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+ur=v+u
133 4 adantr φa𝒫AFinb𝒫BFinAB=
134 116 ad2antrl φa𝒫AFinb𝒫BFinaA
135 122 adantl a𝒫AFinb𝒫BFinbB
136 135 adantl φa𝒫AFinb𝒫BFinbB
137 ssin0 AB=aAbBab=
138 133 134 136 137 syl3anc φa𝒫AFinb𝒫BFinab=
139 eqidd φa𝒫AFinb𝒫BFinab=ab
140 108 adantl φa𝒫AFinb𝒫BFinabFin
141 rge0ssre 0+∞
142 ax-resscn
143 141 142 sstri 0+∞
144 5 28 fge0iccico φF:U0+∞
145 144 ad2antrr φa𝒫AFinb𝒫BFinyabF:U0+∞
146 97 sselda a𝒫AFinb𝒫BFinyabyU
147 146 adantll φa𝒫AFinb𝒫BFinyabyU
148 145 147 ffvelrnd φa𝒫AFinb𝒫BFinyabFy0+∞
149 143 148 sselid φa𝒫AFinb𝒫BFinyabFy
150 138 139 140 149 fsumsplit φa𝒫AFinb𝒫BFinyabFy=yaFy+ybFy
151 150 ad2antrr φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+uyabFy=yaFy+ybFy
152 131 132 151 3eqtr4d φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+ur=yabFy
153 sumeq1 x=abyxFy=yabFy
154 153 rspceeqv ab𝒫UFinr=yabFyx𝒫UFinr=yxFy
155 111 152 154 syl2anc φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+ux𝒫UFinr=yxFy
156 56 a1i φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urV
157 82 155 156 elrnmptd φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
158 157 ex φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
159 158 ex φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
160 159 ex φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
161 160 rexlimdvv φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
162 161 imp φa𝒫AFinb𝒫BFinv=yaFAyu=ybFByr=v+urranx𝒫UFinyxFy
163 63 81 162 syl2anc φvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+urranx𝒫UFinyxFy
164 163 ex φvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+urranx𝒫UFinyxFy
165 164 rexlimdvv φvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+urranx𝒫UFinyxFy
166 165 imp φvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+urranx𝒫UFinyxFy
167 55 62 166 syl2anc φrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+urranx𝒫UFinyxFy
168 167 ex φrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+urranx𝒫UFinyxFy
169 82 elrnmpt rranx𝒫UFinyxFyrranx𝒫UFinyxFyx𝒫UFinr=yxFy
170 169 ibi rranx𝒫UFinyxFyx𝒫UFinr=yxFy
171 170 adantl φrranx𝒫UFinyxFyx𝒫UFinr=yxFy
172 nfv xφ
173 nfcv _xr
174 nfmpt1 _xx𝒫UFinyxFy
175 174 nfrn _xranx𝒫UFinyxFy
176 173 175 nfel xrranx𝒫UFinyxFy
177 172 176 nfan xφrranx𝒫UFinyxFy
178 nfmpt1 _xx𝒫AFinyxFAy
179 178 nfrn _xranx𝒫AFinyxFAy
180 nfmpt1 _xx𝒫BFinyxFBy
181 180 nfrn _xranx𝒫BFinyxFBy
182 nfv xr=v+u
183 181 182 nfrex xuranx𝒫BFinyxFByr=v+u
184 179 183 nfrex xvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
185 inss2 xAA
186 185 sseli yxAyA
187 186 adantl x𝒫UFinyxAyA
188 118 eqcomd yAFy=FAy
189 187 188 syl x𝒫UFinyxAFy=FAy
190 189 sumeq2dv x𝒫UFinyxAFy=yxAFAy
191 sumeq1 x=zyxFAy=yzFAy
192 191 cbvmptv x𝒫AFinyxFAy=z𝒫AFinyzFAy
193 vex xV
194 193 inex1 xAV
195 194 elpw xA𝒫AxAA
196 185 195 mpbir xA𝒫A
197 196 a1i x𝒫UFinxA𝒫A
198 elinel2 x𝒫UFinxFin
199 inss1 xAx
200 199 a1i x𝒫UFinxAx
201 ssfi xFinxAxxAFin
202 198 200 201 syl2anc x𝒫UFinxAFin
203 197 202 elind x𝒫UFinxA𝒫AFin
204 eqidd x𝒫UFinyxAFAy=yxAFAy
205 sumeq1 z=xAyzFAy=yxAFAy
206 205 rspceeqv xA𝒫AFinyxAFAy=yxAFAyz𝒫AFinyxAFAy=yzFAy
207 203 204 206 syl2anc x𝒫UFinz𝒫AFinyxAFAy=yzFAy
208 sumex yxAFAyV
209 208 a1i x𝒫UFinyxAFAyV
210 192 207 209 elrnmptd x𝒫UFinyxAFAyranx𝒫AFinyxFAy
211 190 210 eqeltrd x𝒫UFinyxAFyranx𝒫AFinyxFAy
212 211 3ad2ant2 φx𝒫UFinr=yxFyyxAFyranx𝒫AFinyxFAy
213 sumeq1 x=zyxFBy=yzFBy
214 213 cbvmptv x𝒫BFinyxFBy=z𝒫BFinyzFBy
215 inss2 xBB
216 193 inex1 xBV
217 216 elpw xB𝒫BxBB
218 215 217 mpbir xB𝒫B
219 218 a1i φx𝒫UFinr=yxFyxB𝒫B
220 inss1 xBx
221 220 a1i x𝒫UFinxBx
222 ssfi xFinxBxxBFin
223 198 221 222 syl2anc x𝒫UFinxBFin
224 223 3ad2ant2 φx𝒫UFinr=yxFyxBFin
225 219 224 elind φx𝒫UFinr=yxFyxB𝒫BFin
226 215 sseli yxByB
227 124 eqcomd yBFy=FBy
228 226 227 syl yxBFy=FBy
229 228 sumeq2i yxBFy=yxBFBy
230 229 a1i φx𝒫UFinyxBFy=yxBFBy
231 230 3adant3 φx𝒫UFinr=yxFyyxBFy=yxBFBy
232 sumeq1 z=xByzFBy=yxBFBy
233 232 rspceeqv xB𝒫BFinyxBFy=yxBFByz𝒫BFinyxBFy=yzFBy
234 225 231 233 syl2anc φx𝒫UFinr=yxFyz𝒫BFinyxBFy=yzFBy
235 sumex yxBFyV
236 235 a1i φx𝒫UFinr=yxFyyxBFyV
237 214 234 236 elrnmptd φx𝒫UFinr=yxFyyxBFyranx𝒫BFinyxFBy
238 simp3 φx𝒫UFinr=yxFyr=yxFy
239 185 a1i φxAA
240 215 a1i φxBB
241 ssin0 AB=xAAxBBxAxB=
242 4 239 240 241 syl3anc φxAxB=
243 242 adantr φx𝒫UFinxAxB=
244 elinel1 x𝒫UFinx𝒫U
245 elpwi x𝒫UxU
246 244 245 syl x𝒫UFinxU
247 3 ineq2i xU=xAB
248 247 a1i xUxU=xAB
249 dfss xUx=xU
250 249 biimpi xUx=xU
251 indi xAB=xAxB
252 251 eqcomi xAxB=xAB
253 252 a1i xUxAxB=xAB
254 248 250 253 3eqtr4d xUx=xAxB
255 246 254 syl x𝒫UFinx=xAxB
256 255 adantl φx𝒫UFinx=xAxB
257 198 adantl φx𝒫UFinxFin
258 144 ad2antrr φx𝒫UFinyxF:U0+∞
259 246 sselda x𝒫UFinyxyU
260 259 adantll φx𝒫UFinyxyU
261 258 260 ffvelrnd φx𝒫UFinyxFy0+∞
262 143 261 sselid φx𝒫UFinyxFy
263 243 256 257 262 fsumsplit φx𝒫UFinyxFy=yxAFy+yxBFy
264 263 3adant3 φx𝒫UFinr=yxFyyxFy=yxAFy+yxBFy
265 238 264 eqtrd φx𝒫UFinr=yxFyr=yxAFy+yxBFy
266 oveq2 u=yxBFyyxAFy+u=yxAFy+yxBFy
267 266 rspceeqv yxBFyranx𝒫BFinyxFByr=yxAFy+yxBFyuranx𝒫BFinyxFByr=yxAFy+u
268 237 265 267 syl2anc φx𝒫UFinr=yxFyuranx𝒫BFinyxFByr=yxAFy+u
269 oveq1 v=yxAFyv+u=yxAFy+u
270 269 eqeq2d v=yxAFyr=v+ur=yxAFy+u
271 270 rexbidv v=yxAFyuranx𝒫BFinyxFByr=v+uuranx𝒫BFinyxFByr=yxAFy+u
272 271 rspcev yxAFyranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=yxAFy+uvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
273 212 268 272 syl2anc φx𝒫UFinr=yxFyvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
274 273 3exp φx𝒫UFinr=yxFyvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
275 274 adantr φrranx𝒫UFinyxFyx𝒫UFinr=yxFyvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
276 177 184 275 rexlimd φrranx𝒫UFinyxFyx𝒫UFinr=yxFyvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
277 171 276 mpd φrranx𝒫UFinyxFyvranx𝒫AFinyxFAyuranx𝒫BFinyxFByr=v+u
278 277 60 sylibr φrranx𝒫UFinyxFyrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u
279 278 ex φrranx𝒫UFinyxFyrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u
280 168 279 impbid φrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+urranx𝒫UFinyxFy
281 280 alrimiv φrrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+urranx𝒫UFinyxFy
282 dfcleq z|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u=ranx𝒫UFinyxFyrrz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+urranx𝒫UFinyxFy
283 281 282 sylibr φz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u=ranx𝒫UFinyxFy
284 283 supeq1d φsupz|vranx𝒫AFinyxFAyuranx𝒫BFinyxFByz=v+u<=supranx𝒫UFinyxFy<
285 27 54 284 3eqtrrd φsupranx𝒫UFinyxFy<=supranx𝒫AFinyxFAy<+𝑒supranx𝒫BFinyxFBy<
286 15 5 6 sge0supre φsum^F=supranx𝒫UFinyxFy<
287 17 24 oveq12d φsum^FA+𝑒sum^FB=supranx𝒫AFinyxFAy<+𝑒supranx𝒫BFinyxFBy<
288 285 286 287 3eqtr4d φsum^F=sum^FA+𝑒sum^FB
289 rexadd sum^FAsum^FBsum^FA+𝑒sum^FB=sum^FA+sum^FB
290 16 23 289 syl2anc φsum^FA+𝑒sum^FB=sum^FA+sum^FB
291 288 290 eqtrd φsum^F=sum^FA+sum^FB