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 sselid
 |-  ( 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 sselid
 |-  ( ( ( ( ( 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 sselid
 |-  ( ( ( ( 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 sselid
 |-  ( ( ( ( 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 ) ) ) )