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
|
sseldi |
|- ( ( ph /\ k e. A ) -> B e. RR ) |
13 |
11 3
|
sseldi |
|- ( ( 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
|
sseldi |
|- ( ( 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
|
sseldi |
|- ( ( 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 ) ) ) ) |