Metamath Proof Explorer

Theorem esumpcvgval

Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017)

Ref Expression
Hypotheses esumpcvgval.1 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
esumpcvgval.2 
|- ( k = l -> A = B )
esumpcvgval.3 
|- ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> )
Assertion esumpcvgval 
|- ( ph -> sum* k e. NN A = sum_ k e. NN A )

Proof

Step Hyp Ref Expression
1 esumpcvgval.1 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
2 esumpcvgval.2 
 |-  ( k = l -> A = B )
3 esumpcvgval.3 
 |-  ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> )
4 xrltso 
 |-  < Or RR*
5 4 a1i 
 |-  ( ph -> < Or RR* )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 1zzd 
 |-  ( ph -> 1 e. ZZ )
8 eqcom 
 |-  ( k = l <-> l = k )
9 eqcom 
 |-  ( A = B <-> B = A )
10 2 8 9 3imtr3i 
 |-  ( l = k -> B = A )
11 10 cbvmptv 
 |-  ( l e. NN |-> B ) = ( k e. NN |-> A )
12 1 11 fmptd 
 |-  ( ph -> ( l e. NN |-> B ) : NN --> ( 0 [,) +oo ) )
13 12 ffvelrnda 
 |-  ( ( ph /\ x e. NN ) -> ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) )
14 elrege0 
 |-  ( ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( l e. NN |-> B ) ` x ) e. RR /\ 0 <_ ( ( l e. NN |-> B ) ` x ) ) )
15 14 simplbi 
 |-  ( ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) -> ( ( l e. NN |-> B ) ` x ) e. RR )
16 13 15 syl 
 |-  ( ( ph /\ x e. NN ) -> ( ( l e. NN |-> B ) ` x ) e. RR )
17 6 7 16 serfre 
 |-  ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) : NN --> RR )
18 12 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( l e. NN |-> B ) : NN --> ( 0 [,) +oo ) )
19 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
20 19 peano2nnd 
 |-  ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN )
21 18 20 ffvelrnd 
 |-  ( ( ph /\ n e. NN ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) )
22 elrege0 
 |-  ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) <-> ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR /\ 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) )
23 22 simprbi 
 |-  ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) -> 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) )
24 21 23 syl 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) )
25 17 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) e. RR )
26 22 simplbi 
 |-  ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR )
27 21 26 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR )
28 25 27 addge01d 
 |-  ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) <-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) )
29 24 28 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) )
30 19 6 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
31 seqp1 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) = ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) )
32 30 31 syl 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) = ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) )
33 29 32 breqtrrd 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) )
34 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
35 11 fvmpt2 
 |-  ( ( k e. NN /\ A e. ( 0 [,) +oo ) ) -> ( ( l e. NN |-> B ) ` k ) = A )
36 34 1 35 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( l e. NN |-> B ) ` k ) = A )
37 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
38 37 1 sseldi 
 |-  ( ( ph /\ k e. NN ) -> A e. RR )
39 17 feqmptd 
 |-  ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) )
40 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
41 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
42 41 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
43 40 42 36 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( l e. NN |-> B ) ` k ) = A )
44 38 recnd 
 |-  ( ( ph /\ k e. NN ) -> A e. CC )
45 40 42 44 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. CC )
46 43 30 45 fsumser 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
47 46 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) = sum_ k e. ( 1 ... n ) A )
48 47 mpteq2dva 
 |-  ( ph -> ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) )
49 39 48 eqtr2d 
 |-  ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) = seq 1 ( + , ( l e. NN |-> B ) ) )
50 49 3 eqeltrrd 
 |-  ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) e. dom ~~> )
51 6 7 36 38 50 isumrecl 
 |-  ( ph -> sum_ k e. NN A e. RR )
52 1zzd 
 |-  ( ( ph /\ n e. NN ) -> 1 e. ZZ )
53 fzfid 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. Fin )
54 fzssuz 
 |-  ( 1 ... n ) C_ ( ZZ>= ` 1 )
55 54 6 sseqtrri 
 |-  ( 1 ... n ) C_ NN
56 55 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN )
57 36 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( l e. NN |-> B ) ` k ) = A )
58 38 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> A e. RR )
59 1 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
60 elrege0 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
61 60 simprbi 
 |-  ( A e. ( 0 [,) +oo ) -> 0 <_ A )
62 59 61 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> 0 <_ A )
63 50 adantr 
 |-  ( ( ph /\ n e. NN ) -> seq 1 ( + , ( l e. NN |-> B ) ) e. dom ~~> )
64 6 52 53 56 57 58 62 63 isumless 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A <_ sum_ k e. NN A )
65 46 64 eqbrtrrd 
 |-  ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A )
66 65 ralrimiva 
 |-  ( ph -> A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A )
67 brralrspcev 
 |-  ( ( sum_ k e. NN A e. RR /\ A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A ) -> E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s )
68 51 66 67 syl2anc 
 |-  ( ph -> E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s )
69 6 7 17 33 68 climsup 
 |-  ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) ~~> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
70 6 7 69 25 climrecl 
 |-  ( ph -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR )
71 70 rexrd 
 |-  ( ph -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* )
72 eqid 
 |-  ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) = ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A )
73 sumex 
 |-  sum_ k e. b A e. _V
74 72 73 elrnmpti 
 |-  ( x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A )
75 ssnnssfz 
 |-  ( b e. ( ~P NN i^i Fin ) -> E. m e. NN b C_ ( 1 ... m ) )
76 fzfid 
 |-  ( ( ph /\ b C_ ( 1 ... m ) ) -> ( 1 ... m ) e. Fin )
77 elfznn 
 |-  ( k e. ( 1 ... m ) -> k e. NN )
78 77 1 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... m ) ) -> A e. ( 0 [,) +oo ) )
79 60 simplbi 
 |-  ( A e. ( 0 [,) +oo ) -> A e. RR )
80 78 79 syl 
 |-  ( ( ph /\ k e. ( 1 ... m ) ) -> A e. RR )
81 80 adantlr 
 |-  ( ( ( ph /\ b C_ ( 1 ... m ) ) /\ k e. ( 1 ... m ) ) -> A e. RR )
82 78 61 syl 
 |-  ( ( ph /\ k e. ( 1 ... m ) ) -> 0 <_ A )
83 82 adantlr 
 |-  ( ( ( ph /\ b C_ ( 1 ... m ) ) /\ k e. ( 1 ... m ) ) -> 0 <_ A )
84 simpr 
 |-  ( ( ph /\ b C_ ( 1 ... m ) ) -> b C_ ( 1 ... m ) )
85 76 81 83 84 fsumless 
 |-  ( ( ph /\ b C_ ( 1 ... m ) ) -> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A )
86 85 ex 
 |-  ( ph -> ( b C_ ( 1 ... m ) -> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) )
87 86 reximdv 
 |-  ( ph -> ( E. m e. NN b C_ ( 1 ... m ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) )
88 87 imp 
 |-  ( ( ph /\ E. m e. NN b C_ ( 1 ... m ) ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A )
89 75 88 sylan2 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A )
90 breq1 
 |-  ( x = sum_ k e. b A -> ( x <_ sum_ k e. ( 1 ... m ) A <-> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) )
91 90 rexbidv 
 |-  ( x = sum_ k e. b A -> ( E. m e. NN x <_ sum_ k e. ( 1 ... m ) A <-> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) )
92 89 91 syl5ibrcom 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( x = sum_ k e. b A -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) )
93 92 rexlimdva 
 |-  ( ph -> ( E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) )
94 93 imp 
 |-  ( ( ph /\ E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A ) -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A )
95 74 94 sylan2b 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A )
96 simpr 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> x = sum_ k e. b A )
97 inss2 
 |-  ( ~P NN i^i Fin ) C_ Fin
98 simpr 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. ( ~P NN i^i Fin ) )
99 97 98 sseldi 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. Fin )
100 simpll 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> ph )
101 inss1 
 |-  ( ~P NN i^i Fin ) C_ ~P NN
102 simplr 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b e. ( ~P NN i^i Fin ) )
103 101 102 sseldi 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b e. ~P NN )
104 103 elpwid 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b C_ NN )
105 simpr 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> k e. b )
106 104 105 sseldd 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> k e. NN )
107 100 106 1 syl2anc 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. ( 0 [,) +oo ) )
108 107 79 syl 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. RR )
109 99 108 fsumrecl 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> sum_ k e. b A e. RR )
110 109 adantr 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> sum_ k e. b A e. RR )
111 96 110 eqeltrd 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> x e. RR )
112 111 r19.29an 
 |-  ( ( ph /\ E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A ) -> x e. RR )
113 74 112 sylan2b 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> x e. RR )
114 113 adantr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x e. RR )
115 fzfid 
 |-  ( ph -> ( 1 ... m ) e. Fin )
116 115 80 fsumrecl 
 |-  ( ph -> sum_ k e. ( 1 ... m ) A e. RR )
117 116 ad2antrr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A e. RR )
118 70 ad2antrr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR )
119 simprr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x <_ sum_ k e. ( 1 ... m ) A )
120 17 frnd 
 |-  ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR )
121 120 ad2antrr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR )
122 1nn 
 |-  1 e. NN
123 122 ne0ii 
 |-  NN =/= (/)
124 dm0rn0 
 |-  ( dom seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> ran seq 1 ( + , ( l e. NN |-> B ) ) = (/) )
125 17 fdmd 
 |-  ( ph -> dom seq 1 ( + , ( l e. NN |-> B ) ) = NN )
126 125 eqeq1d 
 |-  ( ph -> ( dom seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> NN = (/) ) )
127 124 126 bitr3id 
 |-  ( ph -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> NN = (/) ) )
128 127 necon3bid 
 |-  ( ph -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) <-> NN =/= (/) ) )
129 123 128 mpbiri 
 |-  ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) )
130 129 ad2antrr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) )
131 1z 
 |-  1 e. ZZ
132 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) )
133 131 132 ax-mp 
 |-  seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 )
134 6 fneq2i 
 |-  ( seq 1 ( + , ( l e. NN |-> B ) ) Fn NN <-> seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) )
135 133 134 mpbir 
 |-  seq 1 ( + , ( l e. NN |-> B ) ) Fn NN
136 dffn5 
 |-  ( seq 1 ( + , ( l e. NN |-> B ) ) Fn NN <-> seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) )
137 135 136 mpbi 
 |-  seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
138 fvex 
 |-  ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) e. _V
139 137 138 elrnmpti 
 |-  ( z e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
140 r19.29 
 |-  ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> E. n e. NN ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) )
141 breq1 
 |-  ( z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> ( z <_ s <-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s ) )
142 141 biimparc 
 |-  ( ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s )
143 142 rexlimivw 
 |-  ( E. n e. NN ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s )
144 140 143 syl 
 |-  ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s )
145 139 144 sylan2b 
 |-  ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) -> z <_ s )
146 145 ralrimiva 
 |-  ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s -> A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s )
147 146 reximi 
 |-  ( E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s )
148 68 147 syl 
 |-  ( ph -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s )
149 148 ad2antrr 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s )
150 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
151 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> ph )
152 77 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> k e. NN )
153 151 152 36 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> ( ( l e. NN |-> B ) ` k ) = A )
154 150 6 eleqtrdi 
 |-  ( ( ph /\ m e. NN ) -> m e. ( ZZ>= ` 1 ) )
155 151 152 1 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. ( 0 [,) +oo ) )
156 155 79 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. RR )
157 156 recnd 
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. CC )
158 153 154 157 fsumser 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) )
159 fveq2 
 |-  ( n = m -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) )
160 159 rspceeqv 
 |-  ( ( m e. NN /\ sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) ) -> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
161 150 158 160 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
162 137 138 elrnmpti 
 |-  ( sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
163 161 162 sylibr 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) )
164 163 ad2ant2r 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) )
165 suprub 
 |-  ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) -> sum_ k e. ( 1 ... m ) A <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
166 121 130 149 164 165 syl31anc 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
167 114 117 118 119 166 letrd 
 |-  ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
168 95 167 rexlimddv 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
169 70 adantr 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR )
170 113 169 lenltd 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> ( x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) < x ) )
171 168 170 mpbid 
 |-  ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> -. sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) < x )
172 simpr1r 
 |-  ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x = +oo ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
173 172 3anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
174 71 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* )
175 pnfnlt 
 |-  ( sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* -> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
176 174 175 syl 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
177 breq1 
 |-  ( x = +oo -> ( x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) )
178 177 notbid 
 |-  ( x = +oo -> ( -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) )
179 178 adantl 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> ( -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) )
180 176 179 mpbird 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
181 173 180 pm2.21dd 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
182 simplll 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> ph )
183 simpr1l 
 |-  ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x < +oo ) ) -> x e. RR* )
184 183 3anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x e. RR* )
185 simplr 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> 0 <_ x )
186 simpr 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x < +oo )
187 0xr 
 |-  0 e. RR*
188 pnfxr 
 |-  +oo e. RR*
189 elico1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) ) )
190 187 188 189 mp2an 
 |-  ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) )
191 184 185 186 190 syl3anbrc 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x e. ( 0 [,) +oo ) )
192 simpr1r 
 |-  ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x < +oo ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
193 192 3anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
194 120 adantr 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR )
195 129 adantr 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) )
196 148 adantr 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s )
197 194 195 196 3jca 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) )
198 simprl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x e. ( 0 [,) +oo ) )
199 37 198 sseldi 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x e. RR )
200 simprr 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
201 suprlub 
 |-  ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ x e. RR ) -> ( x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) )
202 201 biimpa 
 |-  ( ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ x e. RR ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) -> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y )
203 197 199 200 202 syl21anc 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y )
204 41 ssriv 
 |-  ( 1 ... n ) C_ NN
205 ovex 
 |-  ( 1 ... n ) e. _V
206 205 elpw 
 |-  ( ( 1 ... n ) e. ~P NN <-> ( 1 ... n ) C_ NN )
207 204 206 mpbir 
 |-  ( 1 ... n ) e. ~P NN
208 fzfi 
 |-  ( 1 ... n ) e. Fin
209 elin 
 |-  ( ( 1 ... n ) e. ( ~P NN i^i Fin ) <-> ( ( 1 ... n ) e. ~P NN /\ ( 1 ... n ) e. Fin ) )
210 207 208 209 mpbir2an 
 |-  ( 1 ... n ) e. ( ~P NN i^i Fin )
211 210 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> ( 1 ... n ) e. ( ~P NN i^i Fin ) )
212 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
213 46 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> sum_ k e. ( 1 ... n ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
214 212 213 eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> y = sum_ k e. ( 1 ... n ) A )
215 sumeq1 
 |-  ( b = ( 1 ... n ) -> sum_ k e. b A = sum_ k e. ( 1 ... n ) A )
216 215 rspceeqv 
 |-  ( ( ( 1 ... n ) e. ( ~P NN i^i Fin ) /\ y = sum_ k e. ( 1 ... n ) A ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A )
217 211 214 216 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A )
218 217 ex 
 |-  ( ( ph /\ n e. NN ) -> ( y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) )
219 218 rexlimdva 
 |-  ( ph -> ( E. n e. NN y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) )
220 137 138 elrnmpti 
 |-  ( y e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) )
221 72 73 elrnmpti 
 |-  ( y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A )
222 219 220 221 3imtr4g 
 |-  ( ph -> ( y e. ran seq 1 ( + , ( l e. NN |-> B ) ) -> y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) )
223 222 ssrdv 
 |-  ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) )
224 ssrexv 
 |-  ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) -> ( E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) )
225 223 224 syl 
 |-  ( ph -> ( E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) )
226 225 imp 
 |-  ( ( ph /\ E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
227 203 226 syldan 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
228 182 191 193 227 syl12anc 
 |-  ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
229 simplrl 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> x e. RR* )
230 xrlelttric 
 |-  ( ( +oo e. RR* /\ x e. RR* ) -> ( +oo <_ x \/ x < +oo ) )
231 188 230 mpan 
 |-  ( x e. RR* -> ( +oo <_ x \/ x < +oo ) )
232 xgepnf 
 |-  ( x e. RR* -> ( +oo <_ x <-> x = +oo ) )
233 232 orbi1d 
 |-  ( x e. RR* -> ( ( +oo <_ x \/ x < +oo ) <-> ( x = +oo \/ x < +oo ) ) )
234 231 233 mpbid 
 |-  ( x e. RR* -> ( x = +oo \/ x < +oo ) )
235 229 234 syl 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> ( x = +oo \/ x < +oo ) )
236 181 228 235 mpjaodan 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
237 0elpw 
 |-  (/) e. ~P NN
238 0fin 
 |-  (/) e. Fin
239 elin 
 |-  ( (/) e. ( ~P NN i^i Fin ) <-> ( (/) e. ~P NN /\ (/) e. Fin ) )
240 237 238 239 mpbir2an 
 |-  (/) e. ( ~P NN i^i Fin )
241 sum0 
 |-  sum_ k e. (/) A = 0
242 241 eqcomi 
 |-  0 = sum_ k e. (/) A
243 sumeq1 
 |-  ( b = (/) -> sum_ k e. b A = sum_ k e. (/) A )
244 243 rspceeqv 
 |-  ( ( (/) e. ( ~P NN i^i Fin ) /\ 0 = sum_ k e. (/) A ) -> E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A )
245 240 242 244 mp2an 
 |-  E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A
246 72 73 elrnmpti 
 |-  ( 0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A )
247 245 246 mpbir 
 |-  0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A )
248 breq2 
 |-  ( y = 0 -> ( x < y <-> x < 0 ) )
249 248 rspcev 
 |-  ( ( 0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) /\ x < 0 ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
250 247 249 mpan 
 |-  ( x < 0 -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
251 250 adantl 
 |-  ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ x < 0 ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
252 xrlelttric 
 |-  ( ( 0 e. RR* /\ x e. RR* ) -> ( 0 <_ x \/ x < 0 ) )
253 187 252 mpan 
 |-  ( x e. RR* -> ( 0 <_ x \/ x < 0 ) )
254 253 ad2antrl 
 |-  ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ( 0 <_ x \/ x < 0 ) )
255 236 251 254 mpjaodan 
 |-  ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y )
256 5 71 171 255 eqsupd 
 |-  ( ph -> sup ( ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) , RR* , < ) = sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
257 nfv 
 |-  F/ k ph
258 nfcv 
 |-  F/_ k NN
259 nnex 
 |-  NN e. _V
260 259 a1i 
 |-  ( ph -> NN e. _V )
261 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
262 261 1 sseldi 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
263 elex 
 |-  ( b e. ( ~P NN i^i Fin ) -> b e. _V )
264 263 adantl 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. _V )
265 107 fmpttd 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( k e. b |-> A ) : b --> ( 0 [,) +oo ) )
266 esumpfinvallem 
 |-  ( ( b e. _V /\ ( k e. b |-> A ) : b --> ( 0 [,) +oo ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) )
267 264 265 266 syl2anc 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) )
268 108 recnd 
 |-  ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. CC )
269 99 268 gsumfsum 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = sum_ k e. b A )
270 267 269 eqtr3d 
 |-  ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) = sum_ k e. b A )
271 257 258 260 262 270 esumval 
 |-  ( ph -> sum* k e. NN A = sup ( ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) , RR* , < ) )
272 6 7 36 44 69 isumclim 
 |-  ( ph -> sum_ k e. NN A = sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) )
273 256 271 272 3eqtr4d 
 |-  ( ph -> sum* k e. NN A = sum_ k e. NN A )