# Metamath Proof Explorer

## Theorem sge0xaddlem2

Description: The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0xaddlem2.a ${⊢}{\phi }\to {A}\in {V}$
sge0xaddlem2.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right)$
sge0xaddlem2.c ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in \left[0,\mathrm{+\infty }\right)$
sge0xaddlem2.sb ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)\in ℝ$
sge0xaddlem2.sc ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\in ℝ$
Assertion sge0xaddlem2 ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}{+}_{𝑒}{C}\right)\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right){+}_{𝑒}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sge0xaddlem2.a ${⊢}{\phi }\to {A}\in {V}$
2 sge0xaddlem2.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right)$
3 sge0xaddlem2.c ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in \left[0,\mathrm{+\infty }\right)$
4 sge0xaddlem2.sb ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)\in ℝ$
5 sge0xaddlem2.sc ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\in ℝ$
6 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
7 0xr ${⊢}0\in {ℝ}^{*}$
8 7 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\in {ℝ}^{*}$
9 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
10 9 a1i ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \mathrm{+\infty }\in {ℝ}^{*}$
11 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
12 11 2 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
13 11 3 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℝ$
14 12 13 readdcld ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}+{C}\in ℝ$
15 14 rexrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}+{C}\in {ℝ}^{*}$
16 icossicc ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$
17 16 2 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
18 xrge0ge0 ${⊢}{B}\in \left[0,\mathrm{+\infty }\right]\to 0\le {B}$
19 17 18 syl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
20 16 3 sseldi ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in \left[0,\mathrm{+\infty }\right]$
21 xrge0ge0 ${⊢}{C}\in \left[0,\mathrm{+\infty }\right]\to 0\le {C}$
22 20 21 syl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {C}$
23 12 13 19 22 addge0d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}+{C}$
24 14 ltpnfd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}+{C}<\mathrm{+\infty }$
25 8 10 15 23 24 elicod ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}+{C}\in \left[0,\mathrm{+\infty }\right)$
26 6 1 25 sge0revalmpt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)$
27 rexadd ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
28 12 13 27 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}{+}_{𝑒}{C}={B}+{C}$
29 28 mpteq2dva ${⊢}{\phi }\to \left({k}\in {A}⟼{B}{+}_{𝑒}{C}\right)=\left({k}\in {A}⟼{B}+{C}\right)$
30 29 fveq2d ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}{+}_{𝑒}{C}\right)\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)$
31 rexadd ${⊢}\left(\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)\in ℝ\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\in ℝ\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right){+}_{𝑒}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$
32 4 5 31 syl2anc ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right){+}_{𝑒}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$
33 6 1 2 sge0revalmpt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)=sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)$
34 6 1 3 sge0revalmpt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)=sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
35 33 34 oveq12d ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)=sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
36 33 eqcomd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)$
37 36 4 eqeltrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)\in ℝ$
38 34 5 eqeltrrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\in ℝ$
39 37 38 readdcld ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\in ℝ$
40 39 rexrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
41 elinel2 ${⊢}{x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {x}\in \mathrm{Fin}$
42 41 adantl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to {x}\in \mathrm{Fin}$
43 simpll ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {\phi }$
44 elpwinss ${⊢}{x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {x}\subseteq {A}$
45 44 adantr ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {x}\right)\to {x}\subseteq {A}$
46 simpr ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {x}\right)\to {k}\in {x}$
47 45 46 sseldd ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {x}\right)\to {k}\in {A}$
48 47 adantll ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {k}\in {A}$
49 43 48 12 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {B}\in ℝ$
50 43 48 13 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {C}\in ℝ$
51 49 50 readdcld ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {B}+{C}\in ℝ$
52 42 51 fsumrecl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}\left({B}+{C}\right)\in ℝ$
53 52 rexrd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}\left({B}+{C}\right)\in {ℝ}^{*}$
54 53 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}\left({B}+{C}\right)\in {ℝ}^{*}$
55 eqid ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right)=\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right)$
56 55 rnmptss ${⊢}\forall {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}\left({B}+{C}\right)\in {ℝ}^{*}\to \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right)\subseteq {ℝ}^{*}$
57 54 56 syl ${⊢}{\phi }\to \mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right)\subseteq {ℝ}^{*}$
58 supxrcl ${⊢}\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right)\subseteq {ℝ}^{*}\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
59 57 58 syl ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)\in {ℝ}^{*}$
60 35 eqcomd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$
61 60 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$
62 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)$
63 1 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to {A}\in {V}$
64 17 adantlr ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
65 rphalfcl ${⊢}{e}\in {ℝ}^{+}\to \frac{{e}}{2}\in {ℝ}^{+}$
66 65 adantl ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \frac{{e}}{2}\in {ℝ}^{+}$
67 4 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)\in ℝ$
68 62 63 64 66 67 sge0ltfirpmpt2 ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)$
69 20 adantlr ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {k}\in {A}\right)\to {C}\in \left[0,\mathrm{+\infty }\right]$
70 5 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\in ℝ$
71 62 63 69 66 70 sge0ltfirpmpt2 ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)$
72 71 3ad2ant1 ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to \exists {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)$
73 63 3ad2ant1 ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to {A}\in {V}$
74 73 3ad2ant1 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {A}\in {V}$
75 simpl1l ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {j}\in {A}\right)\to {\phi }$
76 75 3ad2antl1 ${⊢}\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\wedge {j}\in {A}\right)\to {\phi }$
77 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\wedge {j}\in {A}\right)\to {j}\in {A}$
78 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {A}\right)$
79 nfcsb1v
80 79 nfel1
81 78 80 nfim
82 eleq1w ${⊢}{k}={j}\to \left({k}\in {A}↔{j}\in {A}\right)$
83 82 anbi2d ${⊢}{k}={j}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {j}\in {A}\right)\right)$
84 csbeq1a
85 84 eleq1d
86 83 85 imbi12d
87 81 86 2 chvarfv
88 76 77 87 syl2anc
89 nfcsb1v
90 89 nfel1
91 78 90 nfim
92 csbeq1a
93 92 eleq1d
94 83 93 imbi12d
95 91 94 3 chvarfv
96 76 77 95 syl2anc
97 simp11r ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {e}\in {ℝ}^{+}$
98 simp12 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
99 elpwinss ${⊢}{u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {u}\subseteq {A}$
100 98 99 syl ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {u}\subseteq {A}$
101 elinel2 ${⊢}{u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {u}\in \mathrm{Fin}$
102 101 3ad2ant2 ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to {u}\in \mathrm{Fin}$
103 102 3ad2ant1 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {u}\in \mathrm{Fin}$
104 simp2 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
105 elpwinss ${⊢}{v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {v}\subseteq {A}$
106 104 105 syl ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {v}\subseteq {A}$
107 elinel2 ${⊢}{v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {v}\in \mathrm{Fin}$
108 107 3ad2ant2 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {v}\in \mathrm{Fin}$
109 simp13 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)$
110 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{B}$
111 110 79 84 cbvmpt
112 111 fveq2i
113 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{u}$
114 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{u}$
115 84 113 114 110 79 cbvsum
116 115 oveq1i
117 112 116 breq12i
118 117 biimpi
119 109 118 syl
120 simp3 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)$
121 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
122 121 89 92 cbvmpt
123 122 fveq2i
124 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{v}$
125 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{v}$
126 92 124 125 121 89 cbvsum
127 126 oveq1i
128 123 127 breq12i
129 128 biimpi
130 120 129 syl
131 simp11l ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to {\phi }$
132 84 92 oveq12d
133 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{x}$
134 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{x}$
135 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}\left({B}+{C}\right)$
136 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}+$
137 79 136 89 nfov
138 132 133 134 135 137 cbvsum
139 138 mpteq2i
140 139 rneqi
141 140 supeq1i
142 141 eqcomi
143 142 a1i
144 143 26 eqtr4d
145 ge0xaddcl ${⊢}\left({B}\in \left[0,\mathrm{+\infty }\right]\wedge {C}\in \left[0,\mathrm{+\infty }\right]\right)\to {B}{+}_{𝑒}{C}\in \left[0,\mathrm{+\infty }\right]$
146 17 20 145 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}{+}_{𝑒}{C}\in \left[0,\mathrm{+\infty }\right]$
147 28 146 eqeltrrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}+{C}\in \left[0,\mathrm{+\infty }\right]$
148 6 1 147 sge0clmpt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)\in \left[0,\mathrm{+\infty }\right]$
149 144 148 eqeltrd
150 131 149 syl
151 112 4 eqeltrrid
152 131 151 syl
153 123 5 eqeltrrid
154 131 153 syl
155 74 88 96 97 100 103 106 108 119 130 150 152 154 sge0xaddlem1
156 112 123 oveq12i
157 141 oveq1i
158 156 157 breq12i
159 155 158 sylibr ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\wedge {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}$
160 159 3exp ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to \left({v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to \left(\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}\right)\right)$
161 160 rexlimdv ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to \left(\exists {v}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)<\sum _{{k}\in {v}}{C}+\left(\frac{{e}}{2}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}\right)$
162 72 161 mpd ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}$
163 162 3exp ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left({u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to \left(\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}\right)\right)$
164 163 rexlimdv ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left(\exists {u}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)<\sum _{{k}\in {u}}{B}+\left(\frac{{e}}{2}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}\right)$
165 68 164 mpd ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right)+\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}$
166 61 165 eqbrtrd ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right){+}_{𝑒}{e}$
167 40 59 166 xrlexaddrp ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)$
168 26 eqcomd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)$
169 43 48 25 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {B}+{C}\in \left[0,\mathrm{+\infty }\right)$
170 42 169 sge0fsummpt ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {x}⟼{B}+{C}\right)\right)=\sum _{{k}\in {x}}\left({B}+{C}\right)$
171 49 recnd ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {B}\in ℂ$
172 50 recnd ${⊢}\left(\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {x}\right)\to {C}\in ℂ$
173 42 171 172 fsumadd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}\left({B}+{C}\right)=\sum _{{k}\in {x}}{B}+\sum _{{k}\in {x}}{C}$
174 170 173 eqtrd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {x}⟼{B}+{C}\right)\right)=\sum _{{k}\in {x}}{B}+\sum _{{k}\in {x}}{C}$
175 42 49 fsumrecl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}\in ℝ$
176 42 50 fsumrecl ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{C}\in ℝ$
177 37 adantr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)\in ℝ$
178 38 adantr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\in ℝ$
179 elinel2 ${⊢}{y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {y}\in \mathrm{Fin}$
180 179 adantl ${⊢}\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to {y}\in \mathrm{Fin}$
181 simpll ${⊢}\left(\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {y}\right)\to {\phi }$
182 elpwinss ${⊢}{y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {y}\subseteq {A}$
183 182 adantr ${⊢}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {y}\right)\to {y}\subseteq {A}$
184 simpr ${⊢}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {y}\right)\to {k}\in {y}$
185 183 184 sseldd ${⊢}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {y}\right)\to {k}\in {A}$
186 185 adantll ${⊢}\left(\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {y}\right)\to {k}\in {A}$
187 181 186 12 syl2anc ${⊢}\left(\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {y}\right)\to {B}\in ℝ$
188 180 187 fsumrecl ${⊢}\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {y}}{B}\in ℝ$
189 188 rexrd ${⊢}\left({\phi }\wedge {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {y}}{B}\in {ℝ}^{*}$
190 189 ralrimiva ${⊢}{\phi }\to \forall {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {y}}{B}\in {ℝ}^{*}$
191 eqid ${⊢}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)=\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)$
192 191 rnmptss ${⊢}\forall {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {y}}{B}\in {ℝ}^{*}\to \mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)\subseteq {ℝ}^{*}$
193 190 192 syl ${⊢}{\phi }\to \mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)\subseteq {ℝ}^{*}$
194 193 adantr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)\subseteq {ℝ}^{*}$
195 simpr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)$
196 eqidd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}=\sum _{{k}\in {x}}{B}$
197 sumeq1 ${⊢}{y}={x}\to \sum _{{k}\in {y}}{B}=\sum _{{k}\in {x}}{B}$
198 197 rspceeqv ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \sum _{{k}\in {x}}{B}=\sum _{{k}\in {x}}{B}\right)\to \exists {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}{B}=\sum _{{k}\in {y}}{B}$
199 195 196 198 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \exists {y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}{B}=\sum _{{k}\in {y}}{B}$
200 175 elexd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}\in \mathrm{V}$
201 191 199 200 elrnmptd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}\in \mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)$
202 supxrub ${⊢}\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)\subseteq {ℝ}^{*}\wedge \sum _{{k}\in {x}}{B}\in \mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right)\right)\to \sum _{{k}\in {x}}{B}\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)$
203 194 201 202 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)$
204 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
205 eqid ${⊢}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)=\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)$
206 elinel2 ${⊢}{z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {z}\in \mathrm{Fin}$
207 206 adantl ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to {z}\in \mathrm{Fin}$
208 simpll ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {z}\right)\to {\phi }$
209 elpwinss ${⊢}{z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\to {z}\subseteq {A}$
210 209 adantr ${⊢}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {z}\right)\to {z}\subseteq {A}$
211 simpr ${⊢}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {z}\right)\to {k}\in {z}$
212 210 211 sseldd ${⊢}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge {k}\in {z}\right)\to {k}\in {A}$
213 212 adantll ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {z}\right)\to {k}\in {A}$
214 208 213 13 syl2anc ${⊢}\left(\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\wedge {k}\in {z}\right)\to {C}\in ℝ$
215 207 214 fsumrecl ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {z}}{C}\in ℝ$
216 215 rexrd ${⊢}\left({\phi }\wedge {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {z}}{C}\in {ℝ}^{*}$
217 204 205 216 rnmptssd ${⊢}{\phi }\to \mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)\subseteq {ℝ}^{*}$
218 217 adantr ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)\subseteq {ℝ}^{*}$
219 eqidd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{C}=\sum _{{k}\in {x}}{C}$
220 sumeq1 ${⊢}{z}={x}\to \sum _{{k}\in {z}}{C}=\sum _{{k}\in {x}}{C}$
221 220 rspceeqv ${⊢}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\wedge \sum _{{k}\in {x}}{C}=\sum _{{k}\in {x}}{C}\right)\to \exists {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}{C}=\sum _{{k}\in {z}}{C}$
222 195 219 221 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \exists {z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\sum _{{k}\in {x}}{C}=\sum _{{k}\in {z}}{C}$
223 176 elexd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{C}\in \mathrm{V}$
224 205 222 223 elrnmptd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{C}\in \mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)$
225 supxrub ${⊢}\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)\subseteq {ℝ}^{*}\wedge \sum _{{k}\in {x}}{C}\in \mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right)\right)\to \sum _{{k}\in {x}}{C}\le sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
226 218 224 225 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{C}\le sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
227 175 176 177 178 203 226 le2addd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \sum _{{k}\in {x}}{B}+\sum _{{k}\in {x}}{C}\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
228 174 227 eqbrtrd ${⊢}\left({\phi }\wedge {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\right)\to \mathrm{sum^}\left(\left({k}\in {x}⟼{B}+{C}\right)\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
229 228 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {x}⟼{B}+{C}\right)\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
230 6 1 147 40 sge0lefimpt ${⊢}{\phi }\to \left(\mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)↔\forall {x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}\mathrm{sum^}\left(\left({k}\in {x}⟼{B}+{C}\right)\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)\right)$
231 229 230 mpbird ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}+{C}\right)\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
232 168 231 eqbrtrd ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)\le sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)$
233 40 59 167 232 xrletrid ${⊢}{\phi }\to sup\left(\mathrm{ran}\left({y}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {y}}{B}\right),{ℝ}^{*},<\right)+sup\left(\mathrm{ran}\left({z}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {z}}{C}\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)$
234 32 35 233 3eqtrd ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right){+}_{𝑒}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫{A}\cap \mathrm{Fin}\right)⟼\sum _{{k}\in {x}}\left({B}+{C}\right)\right),{ℝ}^{*},<\right)$
235 26 30 234 3eqtr4d ${⊢}{\phi }\to \mathrm{sum^}\left(\left({k}\in {A}⟼{B}{+}_{𝑒}{C}\right)\right)=\mathrm{sum^}\left(\left({k}\in {A}⟼{B}\right)\right){+}_{𝑒}\mathrm{sum^}\left(\left({k}\in {A}⟼{C}\right)\right)$