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 
|- ( ph -> A e. V )
sge0xaddlem2.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
sge0xaddlem2.c 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,) +oo ) )
sge0xaddlem2.sb 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) e. RR )
sge0xaddlem2.sc 
|- ( ph -> ( sum^ ` ( k e. A |-> C ) ) e. RR )
Assertion sge0xaddlem2 
|- ( ph -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )

Proof

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