Metamath Proof Explorer

Theorem sge0split

Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0split.a 
|- ( ph -> A e. V )
sge0split.b 
|- ( ph -> B e. W )
sge0split.u 
|- U = ( A u. B )
sge0split.in0 
|- ( ph -> ( A i^i B ) = (/) )
sge0split.f 
|- ( ph -> F : U --> ( 0 [,] +oo ) )
Assertion sge0split 
|- ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0split.a 
 |-  ( ph -> A e. V )
2 sge0split.b 
 |-  ( ph -> B e. W )
3 sge0split.u 
 |-  U = ( A u. B )
4 sge0split.in0 
 |-  ( ph -> ( A i^i B ) = (/) )
5 sge0split.f 
 |-  ( ph -> F : U --> ( 0 [,] +oo ) )
6 1 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> A e. V )
7 2 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> B e. W )
8 4 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( A i^i B ) = (/) )
9 5 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> F : U --> ( 0 [,] +oo ) )
10 simpr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) e. RR )
11 6 7 3 8 9 10 sge0resplit 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
12 unexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
13 1 2 12 syl2anc 
 |-  ( ph -> ( A u. B ) e. _V )
14 3 13 eqeltrid 
 |-  ( ph -> U e. _V )
15 14 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> U e. _V )
16 15 9 10 sge0ssre 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` A ) ) e. RR )
17 15 9 10 sge0ssre 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` B ) ) e. RR )
18 rexadd 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR /\ ( sum^ ` ( F |` B ) ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
19 16 17 18 syl2anc 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) )
20 19 eqcomd 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( ( sum^ ` ( F |` A ) ) + ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
21 11 20 eqtrd 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
22 simpl 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ph )
23 simpr 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> -. ( sum^ ` F ) e. RR )
24 14 5 sge0repnf 
 |-  ( ph -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
25 24 adantr 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
26 23 25 mtbid 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> -. -. ( sum^ ` F ) = +oo )
27 26 notnotrd 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = +oo )
28 14 5 sge0xrcl 
 |-  ( ph -> ( sum^ ` F ) e. RR* )
29 28 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. RR* )
30 ssun1 
 |-  A C_ ( A u. B )
31 30 3 sseqtrri 
 |-  A C_ U
32 31 a1i 
 |-  ( ph -> A C_ U )
33 5 32 fssresd 
 |-  ( ph -> ( F |` A ) : A --> ( 0 [,] +oo ) )
34 1 33 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) e. RR* )
35 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
36 ssun2 
 |-  B C_ ( A u. B )
37 36 3 sseqtrri 
 |-  B C_ U
38 37 a1i 
 |-  ( ph -> B C_ U )
39 5 38 fssresd 
 |-  ( ph -> ( F |` B ) : B --> ( 0 [,] +oo ) )
40 2 39 sge0cl 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) e. ( 0 [,] +oo ) )
41 35 40 sseldi 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) e. RR* )
42 34 41 xaddcld 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* )
43 42 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* )
44 pnfxr 
 |-  +oo e. RR*
45 eqid 
 |-  +oo = +oo
46 xreqle 
 |-  ( ( +oo e. RR* /\ +oo = +oo ) -> +oo <_ +oo )
47 44 45 46 mp2an 
 |-  +oo <_ +oo
48 47 a1i 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo <_ +oo )
49 14 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> U e. _V )
50 5 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> F : U --> ( 0 [,] +oo ) )
51 rnresss 
 |-  ran ( F |` A ) C_ ran F
52 51 sseli 
 |-  ( +oo e. ran ( F |` A ) -> +oo e. ran F )
53 52 adantl 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo e. ran F )
54 49 50 53 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) = +oo )
55 xrge0neqmnf 
 |-  ( ( sum^ ` ( F |` B ) ) e. ( 0 [,] +oo ) -> ( sum^ ` ( F |` B ) ) =/= -oo )
56 40 55 syl 
 |-  ( ph -> ( sum^ ` ( F |` B ) ) =/= -oo )
57 xaddpnf2 
 |-  ( ( ( sum^ ` ( F |` B ) ) e. RR* /\ ( sum^ ` ( F |` B ) ) =/= -oo ) -> ( +oo +e ( sum^ ` ( F |` B ) ) ) = +oo )
58 41 56 57 syl2anc 
 |-  ( ph -> ( +oo +e ( sum^ ` ( F |` B ) ) ) = +oo )
59 58 eqcomd 
 |-  ( ph -> +oo = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
60 59 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
61 1 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> A e. V )
62 33 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
63 simpr 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> +oo e. ran ( F |` A ) )
64 61 62 63 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) = +oo )
65 64 oveq1d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( +oo +e ( sum^ ` ( F |` B ) ) ) )
66 60 54 65 3eqtr4d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
67 66 54 eqtr3d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = +oo )
68 54 67 breq12d 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <-> +oo <_ +oo ) )
69 48 68 mpbird 
 |-  ( ( ph /\ +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
70 47 a1i 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo <_ +oo )
71 14 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> U e. _V )
72 5 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,] +oo ) )
73 rnresss 
 |-  ran ( F |` B ) C_ ran F
74 73 sseli 
 |-  ( +oo e. ran ( F |` B ) -> +oo e. ran F )
75 74 adantl 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo e. ran F )
76 71 72 75 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) = +oo )
77 2 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> B e. W )
78 39 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
79 simpr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> +oo e. ran ( F |` B ) )
80 77 78 79 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = +oo )
81 80 oveq2d 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( ( sum^ ` ( F |` A ) ) +e +oo ) )
82 1 33 sge0cl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) e. ( 0 [,] +oo ) )
83 xrge0neqmnf 
 |-  ( ( sum^ ` ( F |` A ) ) e. ( 0 [,] +oo ) -> ( sum^ ` ( F |` A ) ) =/= -oo )
84 82 83 syl 
 |-  ( ph -> ( sum^ ` ( F |` A ) ) =/= -oo )
85 xaddpnf1 
 |-  ( ( ( sum^ ` ( F |` A ) ) e. RR* /\ ( sum^ ` ( F |` A ) ) =/= -oo ) -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
86 34 84 85 syl2anc 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
87 86 adantr 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e +oo ) = +oo )
88 81 87 eqtrd 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = +oo )
89 76 88 breq12d 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <-> +oo <_ +oo ) )
90 70 89 mpbird 
 |-  ( ( ph /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
91 90 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
92 simpr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
93 vex 
 |-  z e. _V
94 eqid 
 |-  ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) )
95 94 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) ) )
96 93 95 ax-mp 
 |-  ( z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) )
97 92 96 sylib 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) )
98 simp3 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> z = sum_ y e. x ( F ` y ) )
99 inss1 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( x i^i A )
100 inss2 
 |-  ( x i^i A ) C_ A
101 99 100 sstri 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ A
102 inss2 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( x i^i B )
103 inss2 
 |-  ( x i^i B ) C_ B
104 102 103 sstri 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ B
105 101 104 ssini 
 |-  ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( A i^i B )
106 105 a1i 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) C_ ( A i^i B ) )
107 106 4 sseqtrd 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) C_ (/) )
108 ss0 
 |-  ( ( ( x i^i A ) i^i ( x i^i B ) ) C_ (/) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
109 107 108 syl 
 |-  ( ph -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
110 109 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( ( x i^i A ) i^i ( x i^i B ) ) = (/) )
111 indi 
 |-  ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( x i^i B ) )
112 111 eqcomi 
 |-  ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) )
113 112 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( ( x i^i A ) u. ( x i^i B ) ) = ( x i^i ( A u. B ) ) )
114 3 eqcomi 
 |-  ( A u. B ) = U
115 114 ineq2i 
 |-  ( x i^i ( A u. B ) ) = ( x i^i U )
116 115 a1i 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i ( A u. B ) ) = ( x i^i U ) )
117 elinel1 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. ~P U )
118 elpwi 
 |-  ( x e. ~P U -> x C_ U )
119 117 118 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> x C_ U )
120 df-ss 
 |-  ( x C_ U <-> ( x i^i U ) = x )
121 120 biimpi 
 |-  ( x C_ U -> ( x i^i U ) = x )
122 119 121 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i U ) = x )
123 113 116 122 3eqtrrd 
 |-  ( x e. ( ~P U i^i Fin ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
124 123 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> x = ( ( x i^i A ) u. ( x i^i B ) ) )
125 elinel2 
 |-  ( x e. ( ~P U i^i Fin ) -> x e. Fin )
126 125 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> x e. Fin )
127 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
128 5 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,] +oo ) )
129 pm4.56 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) <-> -. ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
130 129 biimpi 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) -> -. ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
131 elun 
 |-  ( +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) <-> ( +oo e. ran ( F |` A ) \/ +oo e. ran ( F |` B ) ) )
132 130 131 sylnibr 
 |-  ( ( -. +oo e. ran ( F |` A ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) )
133 132 adantll 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ( ran ( F |` A ) u. ran ( F |` B ) ) )
134 rnresun 
 |-  ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )
135 134 eqcomi 
 |-  ( ran ( F |` A ) u. ran ( F |` B ) ) = ran ( F |` ( A u. B ) )
136 135 a1i 
 |-  ( ph -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran ( F |` ( A u. B ) ) )
137 114 reseq2i 
 |-  ( F |` ( A u. B ) ) = ( F |` U )
138 137 rneqi 
 |-  ran ( F |` ( A u. B ) ) = ran ( F |` U )
139 138 a1i 
 |-  ( ph -> ran ( F |` ( A u. B ) ) = ran ( F |` U ) )
140 ffn 
 |-  ( F : U --> ( 0 [,] +oo ) -> F Fn U )
141 fnresdm 
 |-  ( F Fn U -> ( F |` U ) = F )
142 5 140 141 3syl 
 |-  ( ph -> ( F |` U ) = F )
143 142 rneqd 
 |-  ( ph -> ran ( F |` U ) = ran F )
144 136 139 143 3eqtrd 
 |-  ( ph -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran F )
145 144 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( ran ( F |` A ) u. ran ( F |` B ) ) = ran F )
146 133 145 neleqtrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ran F )
147 128 146 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> F : U --> ( 0 [,) +oo ) )
148 147 ad2antrr 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> F : U --> ( 0 [,) +oo ) )
149 119 adantr 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> x C_ U )
150 simpr 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. x )
151 149 150 sseldd 
 |-  ( ( x e. ( ~P U i^i Fin ) /\ y e. x ) -> y e. U )
152 151 adantll 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> y e. U )
153 148 152 ffvelrnd 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,) +oo ) )
154 127 153 sseldi 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
155 154 recnd 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. CC )
156 110 124 126 155 fsumsplit 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
157 infi 
 |-  ( x e. Fin -> ( x i^i A ) e. Fin )
158 125 157 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i A ) e. Fin )
159 158 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) e. Fin )
160 simpl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) )
161 elinel1 
 |-  ( y e. ( x i^i A ) -> y e. x )
162 161 adantl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> y e. x )
163 160 162 154 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( F ` y ) e. RR )
164 159 163 fsumrecl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. RR )
165 infi 
 |-  ( x e. Fin -> ( x i^i B ) e. Fin )
166 125 165 syl 
 |-  ( x e. ( ~P U i^i Fin ) -> ( x i^i B ) e. Fin )
167 166 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) e. Fin )
168 simpl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) )
169 elinel1 
 |-  ( y e. ( x i^i B ) -> y e. x )
170 169 adantl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> y e. x )
171 168 170 154 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( F ` y ) e. RR )
172 167 171 fsumrecl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. RR )
173 rexadd 
 |-  ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
174 164 172 173 syl2anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) )
175 174 eqcomd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) + sum_ y e. ( x i^i B ) ( F ` y ) ) = ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) )
176 156 175 eqtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) = ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) )
177 ressxr 
 |-  RR C_ RR*
178 177 164 sseldi 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) e. RR* )
179 177 172 sseldi 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) e. RR* )
180 1 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> A e. V )
181 33 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
182 simpr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> -. +oo e. ran ( F |` A ) )
183 181 182 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( F |` A ) : A --> ( 0 [,) +oo ) )
184 180 183 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
185 184 eqcomd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) = ( sum^ ` ( F |` A ) ) )
186 34 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` ( F |` A ) ) e. RR* )
187 185 186 eqeltrd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* )
188 187 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* )
189 2 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> B e. W )
190 39 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
191 simpr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> -. +oo e. ran ( F |` B ) )
192 190 191 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( F |` B ) : B --> ( 0 [,) +oo ) )
193 189 192 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
194 193 eqcomd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) = ( sum^ ` ( F |` B ) ) )
195 41 adantr 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) e. RR* )
196 194 195 eqeltrd 
 |-  ( ( ph /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* )
197 196 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* )
198 188 197 jca 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) )
199 198 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) )
200 178 179 199 jca31 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR* /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR* ) /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) ) )
201 180 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> A e. V )
202 181 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` A ) : A --> ( 0 [,] +oo ) )
203 182 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> -. +oo e. ran ( F |` A ) )
204 202 203 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` A ) : A --> ( 0 [,) +oo ) )
205 100 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) C_ A )
206 158 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i A ) e. Fin )
207 201 204 205 206 fsumlesge0 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) <_ ( sum^ ` ( F |` A ) ) )
208 100 sseli 
 |-  ( y e. ( x i^i A ) -> y e. A )
209 fvres 
 |-  ( y e. A -> ( ( F |` A ) ` y ) = ( F ` y ) )
210 208 209 syl 
 |-  ( y e. ( x i^i A ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
211 210 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i A ) ) -> ( ( F |` A ) ` y ) = ( F ` y ) )
212 211 sumeq2dv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) = sum_ y e. ( x i^i A ) ( F ` y ) )
213 184 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
214 212 213 breq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( ( F |` A ) ` y ) <_ ( sum^ ` ( F |` A ) ) <-> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) ) )
215 207 214 mpbid 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
216 215 adantlr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
217 189 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> B e. W )
218 190 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
219 191 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> -. +oo e. ran ( F |` B ) )
220 218 219 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( F |` B ) : B --> ( 0 [,) +oo ) )
221 103 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) C_ B )
222 166 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( x i^i B ) e. Fin )
223 217 220 221 222 fsumlesge0 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) <_ ( sum^ ` ( F |` B ) ) )
224 103 sseli 
 |-  ( y e. ( x i^i B ) -> y e. B )
225 fvres 
 |-  ( y e. B -> ( ( F |` B ) ` y ) = ( F ` y ) )
226 224 225 syl 
 |-  ( y e. ( x i^i B ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
227 226 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) /\ y e. ( x i^i B ) ) -> ( ( F |` B ) ` y ) = ( F ` y ) )
228 227 sumeq2dv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) = sum_ y e. ( x i^i B ) ( F ` y ) )
229 193 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
230 228 229 breq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i B ) ( ( F |` B ) ` y ) <_ ( sum^ ` ( F |` B ) ) <-> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
231 223 230 mpbid 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
232 231 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
233 216 232 jca 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) /\ sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
234 xle2add 
 |-  ( ( ( sum_ y e. ( x i^i A ) ( F ` y ) e. RR* /\ sum_ y e. ( x i^i B ) ( F ` y ) e. RR* ) /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) e. RR* /\ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) e. RR* ) ) -> ( ( sum_ y e. ( x i^i A ) ( F ` y ) <_ sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) /\ sum_ y e. ( x i^i B ) ( F ` y ) <_ sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
235 200 233 234 sylc 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> ( sum_ y e. ( x i^i A ) ( F ` y ) +e sum_ y e. ( x i^i B ) ( F ` y ) ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
236 176 235 eqbrtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) ) -> sum_ y e. x ( F ` y ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
237 236 3adant3 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> sum_ y e. x ( F ` y ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
238 98 237 eqbrtrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ x e. ( ~P U i^i Fin ) /\ z = sum_ y e. x ( F ` y ) ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
239 238 3exp 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( x e. ( ~P U i^i Fin ) -> ( z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) ) )
240 239 rexlimdv 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
241 240 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( E. x e. ( ~P U i^i Fin ) z = sum_ y e. x ( F ` y ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
242 97 241 mpd 
 |-  ( ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) /\ z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
243 242 ralrimiva 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
244 147 sge0rnre 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
245 177 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> RR C_ RR* )
246 244 245 sstrd 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
247 188 197 xaddcld 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) e. RR* )
248 supxrleub 
 |-  ( ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* /\ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) e. RR* ) -> ( sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) <-> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
249 246 247 248 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) <-> A. z e. ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) z <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) ) )
250 243 249 mpbird 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) <_ ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
251 14 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> U e. _V )
252 251 147 sge0reval 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P U i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
253 184 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` A ) ) = sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) )
254 193 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` ( F |` B ) ) = sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) )
255 253 254 oveq12d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) = ( sup ( ran ( a e. ( ~P A i^i Fin ) |-> sum_ b e. a ( ( F |` A ) ` b ) ) , RR* , < ) +e sup ( ran ( c e. ( ~P B i^i Fin ) |-> sum_ d e. c ( ( F |` B ) ` d ) ) , RR* , < ) ) )
256 250 252 255 3brtr4d 
 |-  ( ( ( ph /\ -. +oo e. ran ( F |` A ) ) /\ -. +oo e. ran ( F |` B ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
257 91 256 pm2.61dan 
 |-  ( ( ph /\ -. +oo e. ran ( F |` A ) ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
258 69 257 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
259 258 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) <_ ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
260 pnfge 
 |-  ( ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) e. RR* -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
261 42 260 syl 
 |-  ( ph -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
262 261 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ +oo )
263 id 
 |-  ( ( sum^ ` F ) = +oo -> ( sum^ ` F ) = +oo )
264 263 eqcomd 
 |-  ( ( sum^ ` F ) = +oo -> +oo = ( sum^ ` F ) )
265 264 adantl 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> +oo = ( sum^ ` F ) )
266 262 265 breqtrd 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) <_ ( sum^ ` F ) )
267 29 43 259 266 xrletrid 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
268 22 27 267 syl2anc 
 |-  ( ( ph /\ -. ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )
269 21 268 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) = ( ( sum^ ` ( F |` A ) ) +e ( sum^ ` ( F |` B ) ) ) )