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 84 110 79 cbvsum 
 |-  sum_ k e. u B = sum_ j e. u [_ j / k ]_ B
114 113 oveq1i 
 |-  ( sum_ k e. u B + ( e / 2 ) ) = ( sum_ j e. u [_ j / k ]_ B + ( e / 2 ) )
115 112 114 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 ) ) )
116 115 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 ) ) )
117 109 116 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 ) ) )
118 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 ) ) )
119 nfcv 
 |-  F/_ j C
120 119 89 92 cbvmpt 
 |-  ( k e. A |-> C ) = ( j e. A |-> [_ j / k ]_ C )
121 120 fveq2i 
 |-  ( sum^ ` ( k e. A |-> C ) ) = ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) )
122 92 119 89 cbvsum 
 |-  sum_ k e. v C = sum_ j e. v [_ j / k ]_ C
123 122 oveq1i 
 |-  ( sum_ k e. v C + ( e / 2 ) ) = ( sum_ j e. v [_ j / k ]_ C + ( e / 2 ) )
124 121 123 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 ) ) )
125 124 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 ) ) )
126 118 125 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 ) ) )
127 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 )
128 84 92 oveq12d 
 |-  ( k = j -> ( B + C ) = ( [_ j / k ]_ B + [_ j / k ]_ C ) )
129 nfcv 
 |-  F/_ j ( B + C )
130 nfcv 
 |-  F/_ k +
131 79 130 89 nfov 
 |-  F/_ k ( [_ j / k ]_ B + [_ j / k ]_ C )
132 128 129 131 cbvsum 
 |-  sum_ k e. x ( B + C ) = sum_ j e. x ( [_ j / k ]_ B + [_ j / k ]_ C )
133 132 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 ) )
134 133 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 ) )
135 134 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* , < )
136 135 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* , < )
137 136 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* , < ) )
138 137 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 ) ) ) )
139 ge0xaddcl 
 |-  ( ( B e. ( 0 [,] +oo ) /\ C e. ( 0 [,] +oo ) ) -> ( B +e C ) e. ( 0 [,] +oo ) )
140 17 20 139 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( B +e C ) e. ( 0 [,] +oo ) )
141 28 140 eqeltrrd 
 |-  ( ( ph /\ k e. A ) -> ( B + C ) e. ( 0 [,] +oo ) )
142 6 1 141 sge0clmpt 
 |-  ( ph -> ( sum^ ` ( k e. A |-> ( B + C ) ) ) e. ( 0 [,] +oo ) )
143 138 142 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 ) )
144 127 143 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 ) )
145 112 4 eqeltrrid 
 |-  ( ph -> ( sum^ ` ( j e. A |-> [_ j / k ]_ B ) ) e. RR )
146 127 145 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 )
147 121 5 eqeltrrid 
 |-  ( ph -> ( sum^ ` ( j e. A |-> [_ j / k ]_ C ) ) e. RR )
148 127 147 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 )
149 74 88 96 97 100 103 106 108 117 126 144 146 148 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 ) )
150 112 121 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 ) ) )
151 135 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 )
152 150 151 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 ) )
153 149 152 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 ) )
154 153 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 ) ) ) )
155 154 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 ) ) )
156 72 155 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 ) )
157 156 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 ) ) ) )
158 157 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 ) ) )
159 68 158 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 ) )
160 61 159 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 ) )
161 40 59 160 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* , < ) )
162 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 ) ) ) )
163 43 48 25 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ( B + C ) e. ( 0 [,) +oo ) )
164 42 163 sge0fsummpt 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( k e. x |-> ( B + C ) ) ) = sum_ k e. x ( B + C ) )
165 49 recnd 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. CC )
166 50 recnd 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> C e. CC )
167 42 165 166 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 ) )
168 164 167 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 ) )
169 42 49 fsumrecl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x B e. RR )
170 42 50 fsumrecl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x C e. RR )
171 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 )
172 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 )
173 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
174 173 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
175 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> ph )
176 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
177 176 adantr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ k e. y ) -> y C_ A )
178 simpr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ k e. y ) -> k e. y )
179 177 178 sseldd 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ k e. y ) -> k e. A )
180 179 adantll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> k e. A )
181 175 180 12 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ k e. y ) -> B e. RR )
182 174 181 fsumrecl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y B e. RR )
183 182 rexrd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ k e. y B e. RR* )
184 183 ralrimiva 
 |-  ( ph -> A. y e. ( ~P A i^i Fin ) sum_ k e. y B e. RR* )
185 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 )
186 185 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* )
187 184 186 syl 
 |-  ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) C_ RR* )
188 187 adantr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ran ( y e. ( ~P A i^i Fin ) |-> sum_ k e. y B ) C_ RR* )
189 simpr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
190 eqidd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x B = sum_ k e. x B )
191 sumeq1 
 |-  ( y = x -> sum_ k e. y B = sum_ k e. x B )
192 191 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 )
193 189 190 192 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 )
194 169 elexd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x B e. _V )
195 185 193 194 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 ) )
196 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* , < ) )
197 188 195 196 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* , < ) )
198 nfv 
 |-  F/ z ph
199 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 )
200 elinel2 
 |-  ( z e. ( ~P A i^i Fin ) -> z e. Fin )
201 200 adantl 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin )
202 simpll 
 |-  ( ( ( ph /\ z e. ( ~P A i^i Fin ) ) /\ k e. z ) -> ph )
203 elpwinss 
 |-  ( z e. ( ~P A i^i Fin ) -> z C_ A )
204 203 adantr 
 |-  ( ( z e. ( ~P A i^i Fin ) /\ k e. z ) -> z C_ A )
205 simpr 
 |-  ( ( z e. ( ~P A i^i Fin ) /\ k e. z ) -> k e. z )
206 204 205 sseldd 
 |-  ( ( z e. ( ~P A i^i Fin ) /\ k e. z ) -> k e. A )
207 206 adantll 
 |-  ( ( ( ph /\ z e. ( ~P A i^i Fin ) ) /\ k e. z ) -> k e. A )
208 202 207 13 syl2anc 
 |-  ( ( ( ph /\ z e. ( ~P A i^i Fin ) ) /\ k e. z ) -> C e. RR )
209 201 208 fsumrecl 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> sum_ k e. z C e. RR )
210 209 rexrd 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> sum_ k e. z C e. RR* )
211 198 199 210 rnmptssd 
 |-  ( ph -> ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) C_ RR* )
212 211 adantr 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ran ( z e. ( ~P A i^i Fin ) |-> sum_ k e. z C ) C_ RR* )
213 eqidd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x C = sum_ k e. x C )
214 sumeq1 
 |-  ( z = x -> sum_ k e. z C = sum_ k e. x C )
215 214 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 )
216 189 213 215 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 )
217 170 elexd 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ k e. x C e. _V )
218 199 216 217 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 ) )
219 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* , < ) )
220 212 218 219 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* , < ) )
221 169 170 171 172 197 220 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* , < ) ) )
222 168 221 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* , < ) ) )
223 222 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* , < ) ) )
224 6 1 141 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* , < ) ) ) )
225 223 224 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* , < ) ) )
226 162 225 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* , < ) ) )
227 40 59 161 226 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* , < ) )
228 32 35 227 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* , < ) )
229 26 30 228 3eqtr4d 
 |-  ( ph -> ( sum^ ` ( k e. A |-> ( B +e C ) ) ) = ( ( sum^ ` ( k e. A |-> B ) ) +e ( sum^ ` ( k e. A |-> C ) ) ) )