Metamath Proof Explorer

Theorem sge0xaddlem1

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

Ref Expression
Hypotheses sge0xaddlem1.a 
|- ( ph -> A e. V )
sge0xaddlem1.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
sge0xaddlem1.c 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,) +oo ) )
sge0xaddlem1.rp 
|- ( ph -> E e. RR+ )
sge0xaddlem1.u 
|- ( ph -> U C_ A )
sge0xaddlem1.ufi 
|- ( ph -> U e. Fin )
sge0xaddlem1.7 
|- ( ph -> W C_ A )
sge0xaddlem1.wfi 
|- ( ph -> W e. Fin )
sge0xaddlem1.ltb 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) < ( sum_ k e. U B + ( E / 2 ) ) )
sge0xaddlem1.ltc 
|- ( ph -> ( sum^ ` ( k e. A |-> C ) ) < ( sum_ k e. W C + ( E / 2 ) ) )
sge0xaddlem1.xr 
|- ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. ( 0 [,] +oo ) )
sge0xaddlem1.sb 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
sge0xaddlem1.sc 
|- ( ph -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
Assertion sge0xaddlem1 
|- ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )

Proof

Step Hyp Ref Expression
1 sge0xaddlem1.a 
 |-  ( ph -> A e. V )
2 sge0xaddlem1.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
3 sge0xaddlem1.c 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,) +oo ) )
4 sge0xaddlem1.rp 
 |-  ( ph -> E e. RR+ )
5 sge0xaddlem1.u 
 |-  ( ph -> U C_ A )
6 sge0xaddlem1.ufi 
 |-  ( ph -> U e. Fin )
7 sge0xaddlem1.7 
 |-  ( ph -> W C_ A )
8 sge0xaddlem1.wfi 
 |-  ( ph -> W e. Fin )
9 sge0xaddlem1.ltb 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) < ( sum_ k e. U B + ( E / 2 ) ) )
10 sge0xaddlem1.ltc 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) < ( sum_ k e. W C + ( E / 2 ) ) )
11 sge0xaddlem1.xr 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. ( 0 [,] +oo ) )
12 sge0xaddlem1.sb 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
13 sge0xaddlem1.sc 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
14 nfv 
 |-  F/ k ph
15 14 1 2 sge0revalmpt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) )
16 14 1 3 sge0revalmpt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> C ) ) = sup ( ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) , RR* , < ) )
17 15 16 oveq12d 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) = ( sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) + sup ( ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) , RR* , < ) ) )
18 15 eqcomd 
 |-  ( ph -> sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) = ( sum^ ` ( k e. A |-> B ) ) )
19 18 12 eqeltrd 
 |-  ( ph -> sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) e. RR )
20 16 13 eqeltrrd 
 |-  ( ph -> sup ( ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) , RR* , < ) e. RR )
21 19 20 readdcld 
 |-  ( ph -> ( sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) + sup ( ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) , RR* , < ) ) e. RR )
22 21 rexrd 
 |-  ( ph -> ( sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) , RR* , < ) + sup ( ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) , RR* , < ) ) e. RR* )
23 17 22 eqeltrd 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) e. RR* )
24 elinel2 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. Fin )
25 24 adantl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
26 simpll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ph )
27 elpwinss 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
28 27 adantr 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ k e. x ) -> x C_ A )
29 simpr 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ k e. x ) -> k e. x )
30 28 29 sseldd 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ k e. x ) -> k e. A )
31 30 adantll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. A )
32 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
33 32 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
34 26 31 33 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. RR )
35 32 3 sselid 
 |-  ( ( ph /\ k e. A ) -> C e. RR )
36 26 31 35 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> C e. RR )
37 34 36 readdcld 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ( B + C ) e. RR )
38 25 37 fsumrecl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x ( B + C ) e. RR )
39 38 rexrd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x ( B + C ) e. RR* )
40 39 ralrimiva 
 |-  ( ph -> A. x e. ( ~P A i^i Fin ) sum_ k e. x ( B + C ) e. RR* )
41 eqid 
 |-  ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) = ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) )
42 41 rnmptss 
 |-  ( A. x e. ( ~P A i^i Fin ) sum_ k e. x ( B + C ) e. RR* -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) C_ RR* )
43 40 42 syl 
 |-  ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) C_ RR* )
44 supxrcl 
 |-  ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) C_ RR* -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR* )
45 43 44 syl 
 |-  ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR* )
46 4 rpxrd 
 |-  ( ph -> E e. RR* )
47 45 46 xaddcld 
 |-  ( ph -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) e. RR* )
48 simpl 
 |-  ( ( ph /\ k e. U ) -> ph )
49 5 sselda 
 |-  ( ( ph /\ k e. U ) -> k e. A )
50 48 49 2 syl2anc 
 |-  ( ( ph /\ k e. U ) -> B e. ( 0 [,) +oo ) )
51 32 50 sselid 
 |-  ( ( ph /\ k e. U ) -> B e. RR )
52 6 51 fsumrecl 
 |-  ( ph -> sum_ k e. U B e. RR )
53 4 rpred 
 |-  ( ph -> E e. RR )
54 53 rehalfcld 
 |-  ( ph -> ( E / 2 ) e. RR )
55 52 54 readdcld 
 |-  ( ph -> ( sum_ k e. U B + ( E / 2 ) ) e. RR )
56 32 a1i 
 |-  ( ( ph /\ k e. W ) -> ( 0 [,) +oo ) C_ RR )
57 simpl 
 |-  ( ( ph /\ k e. W ) -> ph )
58 7 adantr 
 |-  ( ( ph /\ k e. W ) -> W C_ A )
59 simpr 
 |-  ( ( ph /\ k e. W ) -> k e. W )
60 58 59 sseldd 
 |-  ( ( ph /\ k e. W ) -> k e. A )
61 57 60 3 syl2anc 
 |-  ( ( ph /\ k e. W ) -> C e. ( 0 [,) +oo ) )
62 56 61 sseldd 
 |-  ( ( ph /\ k e. W ) -> C e. RR )
63 8 62 fsumrecl 
 |-  ( ph -> sum_ k e. W C e. RR )
64 63 54 readdcld 
 |-  ( ph -> ( sum_ k e. W C + ( E / 2 ) ) e. RR )
65 55 64 readdcld 
 |-  ( ph -> ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) e. RR )
66 65 rexrd 
 |-  ( ph -> ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) e. RR* )
67 12 13 55 64 9 10 ltadd12dd 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) < ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) )
68 52 recnd 
 |-  ( ph -> sum_ k e. U B e. CC )
69 54 recnd 
 |-  ( ph -> ( E / 2 ) e. CC )
70 63 recnd 
 |-  ( ph -> sum_ k e. W C e. CC )
71 68 69 70 69 add4d 
 |-  ( ph -> ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) = ( ( sum_ k e. U B + sum_ k e. W C ) + ( ( E / 2 ) + ( E / 2 ) ) ) )
72 53 recnd 
 |-  ( ph -> E e. CC )
73 72 2halvesd 
 |-  ( ph -> ( ( E / 2 ) + ( E / 2 ) ) = E )
74 73 oveq2d 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + ( ( E / 2 ) + ( E / 2 ) ) ) = ( ( sum_ k e. U B + sum_ k e. W C ) + E ) )
75 71 74 eqtrd 
 |-  ( ph -> ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) = ( ( sum_ k e. U B + sum_ k e. W C ) + E ) )
76 75 66 eqeltrrd 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) e. RR* )
77 pnfxr 
 |-  +oo e. RR*
78 77 a1i 
 |-  ( ph -> +oo e. RR* )
79 75 65 eqeltrrd 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) e. RR )
80 ltpnf 
 |-  ( ( ( sum_ k e. U B + sum_ k e. W C ) + E ) e. RR -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) < +oo )
81 79 80 syl 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) < +oo )
82 76 78 81 xrltled 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ +oo )
83 82 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ +oo )
84 oveq1 
 |-  ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) = ( +oo +e E ) )
85 84 adantl 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) = ( +oo +e E ) )
86 53 renemnfd 
 |-  ( ph -> E =/= -oo )
87 xaddpnf2 
 |-  ( ( E e. RR* /\ E =/= -oo ) -> ( +oo +e E ) = +oo )
88 46 86 87 syl2anc 
 |-  ( ph -> ( +oo +e E ) = +oo )
89 88 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ( +oo +e E ) = +oo )
90 85 89 eqtr2d 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> +oo = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
91 83 90 breqtrd 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
92 simpl 
 |-  ( ( ph /\ -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ph )
93 92 11 syl 
 |-  ( ( ph /\ -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. ( 0 [,] +oo ) )
94 neqne 
 |-  ( -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) =/= +oo )
95 94 adantl 
 |-  ( ( ph /\ -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) =/= +oo )
96 ge0xrre 
 |-  ( ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. ( 0 [,] +oo ) /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) =/= +oo ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR )
97 93 95 96 syl2anc 
 |-  ( ( ph /\ -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR )
98 52 63 readdcld 
 |-  ( ph -> ( sum_ k e. U B + sum_ k e. W C ) e. RR )
99 98 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( sum_ k e. U B + sum_ k e. W C ) e. RR )
100 simpr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR )
101 53 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> E e. RR )
102 6 8 jca 
 |-  ( ph -> ( U e. Fin /\ W e. Fin ) )
103 unfi 
 |-  ( ( U e. Fin /\ W e. Fin ) -> ( U u. W ) e. Fin )
104 102 103 syl 
 |-  ( ph -> ( U u. W ) e. Fin )
105 simpl 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> ph )
106 5 7 unssd 
 |-  ( ph -> ( U u. W ) C_ A )
107 106 adantr 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> ( U u. W ) C_ A )
108 simpr 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> k e. ( U u. W ) )
109 107 108 sseldd 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> k e. A )
110 105 109 33 syl2anc 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> B e. RR )
111 109 35 syldan 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> C e. RR )
112 110 111 readdcld 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> ( B + C ) e. RR )
113 104 112 fsumrecl 
 |-  ( ph -> sum_ k e. ( U u. W ) ( B + C ) e. RR )
114 113 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> sum_ k e. ( U u. W ) ( B + C ) e. RR )
115 104 110 fsumrecl 
 |-  ( ph -> sum_ k e. ( U u. W ) B e. RR )
116 104 111 fsumrecl 
 |-  ( ph -> sum_ k e. ( U u. W ) C e. RR )
117 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
118 117 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
119 xrge0ge0 
 |-  ( B e. ( 0 [,] +oo ) -> 0 <_ B )
120 118 119 syl 
 |-  ( ( ph /\ k e. A ) -> 0 <_ B )
121 109 120 syldan 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> 0 <_ B )
122 ssun1 
 |-  U C_ ( U u. W )
123 122 a1i 
 |-  ( ph -> U C_ ( U u. W ) )
124 104 110 121 123 fsumless 
 |-  ( ph -> sum_ k e. U B <_ sum_ k e. ( U u. W ) B )
125 117 3 sselid 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
126 xrge0ge0 
 |-  ( C e. ( 0 [,] +oo ) -> 0 <_ C )
127 125 126 syl 
 |-  ( ( ph /\ k e. A ) -> 0 <_ C )
128 109 127 syldan 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> 0 <_ C )
129 ssun2 
 |-  W C_ ( U u. W )
130 129 a1i 
 |-  ( ph -> W C_ ( U u. W ) )
131 104 111 128 130 fsumless 
 |-  ( ph -> sum_ k e. W C <_ sum_ k e. ( U u. W ) C )
132 52 63 115 116 124 131 leadd12dd 
 |-  ( ph -> ( sum_ k e. U B + sum_ k e. W C ) <_ ( sum_ k e. ( U u. W ) B + sum_ k e. ( U u. W ) C ) )
133 110 recnd 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> B e. CC )
134 111 recnd 
 |-  ( ( ph /\ k e. ( U u. W ) ) -> C e. CC )
135 104 133 134 fsumadd 
 |-  ( ph -> sum_ k e. ( U u. W ) ( B + C ) = ( sum_ k e. ( U u. W ) B + sum_ k e. ( U u. W ) C ) )
136 135 eqcomd 
 |-  ( ph -> ( sum_ k e. ( U u. W ) B + sum_ k e. ( U u. W ) C ) = sum_ k e. ( U u. W ) ( B + C ) )
137 132 136 breqtrd 
 |-  ( ph -> ( sum_ k e. U B + sum_ k e. W C ) <_ sum_ k e. ( U u. W ) ( B + C ) )
138 137 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( sum_ k e. U B + sum_ k e. W C ) <_ sum_ k e. ( U u. W ) ( B + C ) )
139 43 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) C_ RR* )
140 104 106 elpwd 
 |-  ( ph -> ( U u. W ) e. ~P A )
141 140 104 elind 
 |-  ( ph -> ( U u. W ) e. ( ~P A i^i Fin ) )
142 113 elexd 
 |-  ( ph -> sum_ k e. ( U u. W ) ( B + C ) e. _V )
143 sumeq1 
 |-  ( x = ( U u. W ) -> sum_ k e. x ( B + C ) = sum_ k e. ( U u. W ) ( B + C ) )
144 41 143 elrnmpt1s 
 |-  ( ( ( U u. W ) e. ( ~P A i^i Fin ) /\ sum_ k e. ( U u. W ) ( B + C ) e. _V ) -> sum_ k e. ( U u. W ) ( B + C ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) )
145 141 142 144 syl2anc 
 |-  ( ph -> sum_ k e. ( U u. W ) ( B + C ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) )
146 145 adantr 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> sum_ k e. ( U u. W ) ( B + C ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) )
147 supxrub 
 |-  ( ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) C_ RR* /\ sum_ k e. ( U u. W ) ( B + C ) e. ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) ) -> sum_ k e. ( U u. W ) ( B + C ) <_ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) )
148 139 146 147 syl2anc 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> sum_ k e. ( U u. W ) ( B + C ) <_ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) )
149 99 114 100 138 148 letrd 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( sum_ k e. U B + sum_ k e. W C ) <_ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) )
150 99 100 101 149 leadd1dd 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) + E ) )
151 rexadd 
 |-  ( ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR /\ E e. RR ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) + E ) )
152 100 101 151 syl2anc 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) + E ) )
153 152 eqcomd 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) + E ) = ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
154 150 153 breqtrd 
 |-  ( ( ph /\ sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. RR ) -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
155 92 97 154 syl2anc 
 |-  ( ( ph /\ -. sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) = +oo ) -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
156 91 155 pm2.61dan 
 |-  ( ph -> ( ( sum_ k e. U B + sum_ k e. W C ) + E ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
157 75 156 eqbrtrd 
 |-  ( ph -> ( ( sum_ k e. U B + ( E / 2 ) ) + ( sum_ k e. W C + ( E / 2 ) ) ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
158 23 66 47 67 157 xrltletrd 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) < ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
159 23 47 158 xrltled 
 |-  ( ph -> ( ( sum^ ` ( k e. A |-> B ) ) + ( sum^ ` ( k e. A |-> C ) ) ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )