Metamath Proof Explorer

Theorem sge0isum

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0isum.m 
|- ( ph -> M e. ZZ )
sge0isum.z 
|- Z = ( ZZ>= ` M )
sge0isum.f 
|- ( ph -> F : Z --> ( 0 [,) +oo ) )
sge0isum.g 
|- G = seq M ( + , F )
sge0isum.gcnv 
|- ( ph -> G ~~> B )
Assertion sge0isum 
|- ( ph -> ( sum^ ` F ) = B )

Proof

Step Hyp Ref Expression
1 sge0isum.m 
 |-  ( ph -> M e. ZZ )
2 sge0isum.z 
 |-  Z = ( ZZ>= ` M )
3 sge0isum.f 
 |-  ( ph -> F : Z --> ( 0 [,) +oo ) )
4 sge0isum.g 
 |-  G = seq M ( + , F )
5 sge0isum.gcnv 
 |-  ( ph -> G ~~> B )
6 2 fvexi 
 |-  Z e. _V
7 6 a1i 
 |-  ( ph -> Z e. _V )
8 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
9 8 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ ( 0 [,] +oo ) )
10 3 9 fssd 
 |-  ( ph -> F : Z --> ( 0 [,] +oo ) )
11 7 10 sge0xrcl 
 |-  ( ph -> ( sum^ ` F ) e. RR* )
12 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
13 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
14 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( 0 [,) +oo ) )
15 13 14 sselid 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
16 0xr 
 |-  0 e. RR*
17 16 a1i 
 |-  ( ( ph /\ k e. Z ) -> 0 e. RR* )
18 pnfxr 
 |-  +oo e. RR*
19 18 a1i 
 |-  ( ( ph /\ k e. Z ) -> +oo e. RR* )
20 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` k ) e. ( 0 [,) +oo ) ) -> 0 <_ ( F ` k ) )
21 17 19 14 20 syl3anc 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
22 seqex 
 |-  seq M ( + , F ) e. _V
23 4 22 eqeltri 
 |-  G e. _V
24 23 a1i 
 |-  ( ph -> G e. _V )
25 climcl 
 |-  ( G ~~> B -> B e. CC )
26 5 25 syl 
 |-  ( ph -> B e. CC )
27 breldmg 
 |-  ( ( G e. _V /\ B e. CC /\ G ~~> B ) -> G e. dom ~~> )
28 24 26 5 27 syl3anc 
 |-  ( ph -> G e. dom ~~> )
29 4 a1i 
 |-  ( ( ph /\ j e. Z ) -> G = seq M ( + , F ) )
30 29 fveq1d 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) = ( seq M ( + , F ) ` j ) )
31 2 eleq2i 
 |-  ( j e. Z <-> j e. ( ZZ>= ` M ) )
32 31 bilani 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
33 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ph )
34 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
35 34 2 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
36 35 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> k e. Z )
37 33 36 15 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. RR )
38 readdcl 
 |-  ( ( k e. RR /\ i e. RR ) -> ( k + i ) e. RR )
39 38 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ ( k e. RR /\ i e. RR ) ) -> ( k + i ) e. RR )
40 32 37 39 seqcl 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
41 30 40 eqeltrd 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) e. RR )
42 41 recnd 
 |-  ( ( ph /\ j e. Z ) -> ( G ` j ) e. CC )
43 42 ralrimiva 
 |-  ( ph -> A. j e. Z ( G ` j ) e. CC )
44 2 climbdd 
 |-  ( ( M e. ZZ /\ G e. dom ~~> /\ A. j e. Z ( G ` j ) e. CC ) -> E. x e. RR A. j e. Z ( abs ` ( G ` j ) ) <_ x )
45 1 28 43 44 syl3anc 
 |-  ( ph -> E. x e. RR A. j e. Z ( abs ` ( G ` j ) ) <_ x )
46 41 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( G ` j ) e. RR )
47 42 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( G ` j ) e. CC )
48 47 abscld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( abs ` ( G ` j ) ) e. RR )
49 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> x e. RR )
50 46 leabsd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( G ` j ) <_ ( abs ` ( G ` j ) ) )
51 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( abs ` ( G ` j ) ) <_ x )
52 46 48 49 50 51 letrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ ( abs ` ( G ` j ) ) <_ x ) -> ( G ` j ) <_ x )
53 52 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. Z ) -> ( ( abs ` ( G ` j ) ) <_ x -> ( G ` j ) <_ x ) )
54 53 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. Z ( abs ` ( G ` j ) ) <_ x -> A. j e. Z ( G ` j ) <_ x ) )
55 54 reximdva 
 |-  ( ph -> ( E. x e. RR A. j e. Z ( abs ` ( G ` j ) ) <_ x -> E. x e. RR A. j e. Z ( G ` j ) <_ x ) )
56 45 55 mpd 
 |-  ( ph -> E. x e. RR A. j e. Z ( G ` j ) <_ x )
57 2 4 1 12 15 21 56 isumsup2 
 |-  ( ph -> G ~~> sup ( ran G , RR , < ) )
58 2 1 57 41 climrecl 
 |-  ( ph -> sup ( ran G , RR , < ) e. RR )
59 58 rexrd 
 |-  ( ph -> sup ( ran G , RR , < ) e. RR* )
60 3 feqmptd 
 |-  ( ph -> F = ( k e. Z |-> ( F ` k ) ) )
61 60 fveq2d 
 |-  ( ph -> ( sum^ ` F ) = ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
62 mpteq1 
 |-  ( y = (/) -> ( k e. y |-> ( F ` k ) ) = ( k e. (/) |-> ( F ` k ) ) )
63 62 fveq2d 
 |-  ( y = (/) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) = ( sum^ ` ( k e. (/) |-> ( F ` k ) ) ) )
64 mpt0 
 |-  ( k e. (/) |-> ( F ` k ) ) = (/)
65 64 fveq2i 
 |-  ( sum^ ` ( k e. (/) |-> ( F ` k ) ) ) = ( sum^ ` (/) )
66 sge00 
 |-  ( sum^ ` (/) ) = 0
67 65 66 eqtri 
 |-  ( sum^ ` ( k e. (/) |-> ( F ` k ) ) ) = 0
68 67 a1i 
 |-  ( y = (/) -> ( sum^ ` ( k e. (/) |-> ( F ` k ) ) ) = 0 )
69 63 68 eqtrd 
 |-  ( y = (/) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) = 0 )
70 69 adantl 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ y = (/) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) = 0 )
71 0red 
 |-  ( ph -> 0 e. RR )
72 38 adantl 
 |-  ( ( ph /\ ( k e. RR /\ i e. RR ) ) -> ( k + i ) e. RR )
73 2 1 15 72 seqf 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
74 4 a1i 
 |-  ( ph -> G = seq M ( + , F ) )
75 74 feq1d 
 |-  ( ph -> ( G : Z --> RR <-> seq M ( + , F ) : Z --> RR ) )
76 73 75 mpbird 
 |-  ( ph -> G : Z --> RR )
77 76 frnd 
 |-  ( ph -> ran G C_ RR )
78 76 ffund 
 |-  ( ph -> Fun G )
79 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
80 1 79 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
81 2 eqcomi 
 |-  ( ZZ>= ` M ) = Z
82 80 81 eleqtrdi 
 |-  ( ph -> M e. Z )
83 76 fdmd 
 |-  ( ph -> dom G = Z )
84 83 eqcomd 
 |-  ( ph -> Z = dom G )
85 82 84 eleqtrd 
 |-  ( ph -> M e. dom G )
86 fvelrn 
 |-  ( ( Fun G /\ M e. dom G ) -> ( G ` M ) e. ran G )
87 78 85 86 syl2anc 
 |-  ( ph -> ( G ` M ) e. ran G )
88 77 87 sseldd 
 |-  ( ph -> ( G ` M ) e. RR )
89 16 a1i 
 |-  ( ph -> 0 e. RR* )
90 18 a1i 
 |-  ( ph -> +oo e. RR* )
91 3 82 ffvelcdmd 
 |-  ( ph -> ( F ` M ) e. ( 0 [,) +oo ) )
92 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` M ) e. ( 0 [,) +oo ) ) -> 0 <_ ( F ` M ) )
93 89 90 91 92 syl3anc 
 |-  ( ph -> 0 <_ ( F ` M ) )
94 4 fveq1i 
 |-  ( G ` M ) = ( seq M ( + , F ) ` M )
95 94 a1i 
 |-  ( ph -> ( G ` M ) = ( seq M ( + , F ) ` M ) )
96 seq1 
 |-  ( M e. ZZ -> ( seq M ( + , F ) ` M ) = ( F ` M ) )
97 1 96 syl 
 |-  ( ph -> ( seq M ( + , F ) ` M ) = ( F ` M ) )
98 95 97 eqtr2d 
 |-  ( ph -> ( F ` M ) = ( G ` M ) )
99 93 98 breqtrd 
 |-  ( ph -> 0 <_ ( G ` M ) )
100 87 ne0d 
 |-  ( ph -> ran G =/= (/) )
101 simpr 
 |-  ( ( ph /\ z e. ran G ) -> z e. ran G )
102 76 ffnd 
 |-  ( ph -> G Fn Z )
103 fvelrnb 
 |-  ( G Fn Z -> ( z e. ran G <-> E. j e. Z ( G ` j ) = z ) )
104 102 103 syl 
 |-  ( ph -> ( z e. ran G <-> E. j e. Z ( G ` j ) = z ) )
105 104 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ( z e. ran G <-> E. j e. Z ( G ` j ) = z ) )
106 101 105 mpbid 
 |-  ( ( ph /\ z e. ran G ) -> E. j e. Z ( G ` j ) = z )
107 106 adantlr 
 |-  ( ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) /\ z e. ran G ) -> E. j e. Z ( G ` j ) = z )
108 nfv 
 |-  F/ j ph
109 nfra1 
 |-  F/ j A. j e. Z ( G ` j ) <_ x
110 108 109 nfan 
 |-  F/ j ( ph /\ A. j e. Z ( G ` j ) <_ x )
111 nfv 
 |-  F/ j z e. ran G
112 110 111 nfan 
 |-  F/ j ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) /\ z e. ran G )
113 nfv 
 |-  F/ j z <_ x
114 rspa 
 |-  ( ( A. j e. Z ( G ` j ) <_ x /\ j e. Z ) -> ( G ` j ) <_ x )
115 114 3adant3 
 |-  ( ( A. j e. Z ( G ` j ) <_ x /\ j e. Z /\ ( G ` j ) = z ) -> ( G ` j ) <_ x )
116 simp3 
 |-  ( ( A. j e. Z ( G ` j ) <_ x /\ j e. Z /\ ( G ` j ) = z ) -> ( G ` j ) = z )
117 id 
 |-  ( ( G ` j ) = z -> ( G ` j ) = z )
118 117 eqcomd 
 |-  ( ( G ` j ) = z -> z = ( G ` j ) )
119 118 adantl 
 |-  ( ( ( G ` j ) <_ x /\ ( G ` j ) = z ) -> z = ( G ` j ) )
120 simpl 
 |-  ( ( ( G ` j ) <_ x /\ ( G ` j ) = z ) -> ( G ` j ) <_ x )
121 119 120 eqbrtrd 
 |-  ( ( ( G ` j ) <_ x /\ ( G ` j ) = z ) -> z <_ x )
122 115 116 121 syl2anc 
 |-  ( ( A. j e. Z ( G ` j ) <_ x /\ j e. Z /\ ( G ` j ) = z ) -> z <_ x )
123 122 3exp 
 |-  ( A. j e. Z ( G ` j ) <_ x -> ( j e. Z -> ( ( G ` j ) = z -> z <_ x ) ) )
124 123 ad2antlr 
 |-  ( ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) /\ z e. ran G ) -> ( j e. Z -> ( ( G ` j ) = z -> z <_ x ) ) )
125 112 113 124 rexlimd 
 |-  ( ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) /\ z e. ran G ) -> ( E. j e. Z ( G ` j ) = z -> z <_ x ) )
126 107 125 mpd 
 |-  ( ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) /\ z e. ran G ) -> z <_ x )
127 126 ralrimiva 
 |-  ( ( ph /\ A. j e. Z ( G ` j ) <_ x ) -> A. z e. ran G z <_ x )
128 127 ex 
 |-  ( ph -> ( A. j e. Z ( G ` j ) <_ x -> A. z e. ran G z <_ x ) )
129 128 reximdv 
 |-  ( ph -> ( E. x e. RR A. j e. Z ( G ` j ) <_ x -> E. x e. RR A. z e. ran G z <_ x ) )
130 56 129 mpd 
 |-  ( ph -> E. x e. RR A. z e. ran G z <_ x )
131 suprub 
 |-  ( ( ( ran G C_ RR /\ ran G =/= (/) /\ E. x e. RR A. z e. ran G z <_ x ) /\ ( G ` M ) e. ran G ) -> ( G ` M ) <_ sup ( ran G , RR , < ) )
132 77 100 130 87 131 syl31anc 
 |-  ( ph -> ( G ` M ) <_ sup ( ran G , RR , < ) )
133 71 88 58 99 132 letrd 
 |-  ( ph -> 0 <_ sup ( ran G , RR , < ) )
134 133 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ y = (/) ) -> 0 <_ sup ( ran G , RR , < ) )
135 70 134 eqbrtrd 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ y = (/) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
136 simpr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> y e. ( ~P Z i^i Fin ) )
137 simpll 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. y ) -> ph )
138 elpwinss 
 |-  ( y e. ( ~P Z i^i Fin ) -> y C_ Z )
139 138 sselda 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ k e. y ) -> k e. Z )
140 139 adantll 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. y ) -> k e. Z )
141 8 14 sselid 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( 0 [,] +oo ) )
142 137 140 141 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. y ) -> ( F ` k ) e. ( 0 [,] +oo ) )
143 eqid 
 |-  ( k e. y |-> ( F ` k ) ) = ( k e. y |-> ( F ` k ) )
144 142 143 fmptd 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( k e. y |-> ( F ` k ) ) : y --> ( 0 [,] +oo ) )
145 136 144 sge0xrcl 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) e. RR* )
146 145 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) e. RR* )
147 fzfid 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( M ... sup ( y , RR , < ) ) e. Fin )
148 elfzuz 
 |-  ( k e. ( M ... sup ( y , RR , < ) ) -> k e. ( ZZ>= ` M ) )
149 148 81 eleqtrdi 
 |-  ( k e. ( M ... sup ( y , RR , < ) ) -> k e. Z )
150 149 141 sylan2 
 |-  ( ( ph /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
151 eqid 
 |-  ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) = ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) )
152 150 151 fmptd 
 |-  ( ph -> ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) : ( M ... sup ( y , RR , < ) ) --> ( 0 [,] +oo ) )
153 152 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) : ( M ... sup ( y , RR , < ) ) --> ( 0 [,] +oo ) )
154 147 153 sge0xrcl 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) e. RR* )
155 154 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) e. RR* )
156 59 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> sup ( ran G , RR , < ) e. RR* )
157 156 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> sup ( ran G , RR , < ) e. RR* )
158 simpll 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ph )
159 149 adantl 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> k e. Z )
160 158 159 141 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) e. ( 0 [,] +oo ) )
161 elinel2 
 |-  ( y e. ( ~P Z i^i Fin ) -> y e. Fin )
162 2 138 161 ssuzfz 
 |-  ( y e. ( ~P Z i^i Fin ) -> y C_ ( M ... sup ( y , RR , < ) ) )
163 162 adantl 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> y C_ ( M ... sup ( y , RR , < ) ) )
164 147 160 163 sge0lessmpt 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) )
165 164 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) )
166 77 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ran G C_ RR )
167 166 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ran G C_ RR )
168 100 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ran G =/= (/) )
169 168 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ran G =/= (/) )
170 130 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> E. x e. RR A. z e. ran G z <_ x )
171 170 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> E. x e. RR A. z e. ran G z <_ x )
172 158 159 14 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) e. ( 0 [,) +oo ) )
173 147 172 sge0fsummpt 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) = sum_ k e. ( M ... sup ( y , RR , < ) ) ( F ` k ) )
174 173 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) = sum_ k e. ( M ... sup ( y , RR , < ) ) ( F ` k ) )
175 eqidd 
 |-  ( ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) = ( F ` k ) )
176 138 2 sseqtrdi 
 |-  ( y e. ( ~P Z i^i Fin ) -> y C_ ( ZZ>= ` M ) )
177 176 adantr 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> y C_ ( ZZ>= ` M ) )
178 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
179 2 178 eqsstri 
 |-  Z C_ ZZ
180 138 179 sstrdi 
 |-  ( y e. ( ~P Z i^i Fin ) -> y C_ ZZ )
181 180 adantr 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> y C_ ZZ )
182 neqne 
 |-  ( -. y = (/) -> y =/= (/) )
183 182 adantl 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> y =/= (/) )
184 161 adantr 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> y e. Fin )
185 suprfinzcl 
 |-  ( ( y C_ ZZ /\ y =/= (/) /\ y e. Fin ) -> sup ( y , RR , < ) e. y )
186 181 183 184 185 syl3anc 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> sup ( y , RR , < ) e. y )
187 177 186 sseldd 
 |-  ( ( y e. ( ~P Z i^i Fin ) /\ -. y = (/) ) -> sup ( y , RR , < ) e. ( ZZ>= ` M ) )
188 187 adantll 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> sup ( y , RR , < ) e. ( ZZ>= ` M ) )
189 15 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
190 158 159 189 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) e. CC )
191 190 adantlr 
 |-  ( ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) /\ k e. ( M ... sup ( y , RR , < ) ) ) -> ( F ` k ) e. CC )
192 175 188 191 fsumser 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> sum_ k e. ( M ... sup ( y , RR , < ) ) ( F ` k ) = ( seq M ( + , F ) ` sup ( y , RR , < ) ) )
193 4 eqcomi 
 |-  seq M ( + , F ) = G
194 193 fveq1i 
 |-  ( seq M ( + , F ) ` sup ( y , RR , < ) ) = ( G ` sup ( y , RR , < ) )
195 194 a1i 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( seq M ( + , F ) ` sup ( y , RR , < ) ) = ( G ` sup ( y , RR , < ) ) )
196 174 192 195 3eqtrd 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) = ( G ` sup ( y , RR , < ) ) )
197 78 adantr 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> Fun G )
198 197 adantr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> Fun G )
199 188 81 eleqtrdi 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> sup ( y , RR , < ) e. Z )
200 84 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> Z = dom G )
201 199 200 eleqtrd 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> sup ( y , RR , < ) e. dom G )
202 fvelrn 
 |-  ( ( Fun G /\ sup ( y , RR , < ) e. dom G ) -> ( G ` sup ( y , RR , < ) ) e. ran G )
203 198 201 202 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( G ` sup ( y , RR , < ) ) e. ran G )
204 196 203 eqeltrd 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) e. ran G )
205 suprub 
 |-  ( ( ( ran G C_ RR /\ ran G =/= (/) /\ E. x e. RR A. z e. ran G z <_ x ) /\ ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) e. ran G ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
206 167 169 171 204 205 syl31anc 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. ( M ... sup ( y , RR , < ) ) |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
207 146 155 157 165 206 xrletrd 
 |-  ( ( ( ph /\ y e. ( ~P Z i^i Fin ) ) /\ -. y = (/) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
208 135 207 pm2.61dan 
 |-  ( ( ph /\ y e. ( ~P Z i^i Fin ) ) -> ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
209 208 ralrimiva 
 |-  ( ph -> A. y e. ( ~P Z i^i Fin ) ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
210 nfv 
 |-  F/ k ph
211 210 7 141 59 sge0lefimpt 
 |-  ( ph -> ( ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) <-> A. y e. ( ~P Z i^i Fin ) ( sum^ ` ( k e. y |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) ) )
212 209 211 mpbird 
 |-  ( ph -> ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) <_ sup ( ran G , RR , < ) )
213 61 212 eqbrtrd 
 |-  ( ph -> ( sum^ ` F ) <_ sup ( ran G , RR , < ) )
214 35 ssriv 
 |-  ( M ... j ) C_ Z
215 214 a1i 
 |-  ( ph -> ( M ... j ) C_ Z )
216 7 141 215 sge0lessmpt 
 |-  ( ph -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
217 216 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
218 fzfid 
 |-  ( ph -> ( M ... j ) e. Fin )
219 35 14 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. ( 0 [,) +oo ) )
220 218 219 sge0fsummpt 
 |-  ( ph -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) = sum_ k e. ( M ... j ) ( F ` k ) )
221 220 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) = sum_ k e. ( M ... j ) ( F ` k ) )
222 33 36 12 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) = ( F ` k ) )
223 33 36 189 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
224 222 32 223 fsumser 
 |-  ( ( ph /\ j e. Z ) -> sum_ k e. ( M ... j ) ( F ` k ) = ( seq M ( + , F ) ` j ) )
225 224 3adant3 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> sum_ k e. ( M ... j ) ( F ` k ) = ( seq M ( + , F ) ` j ) )
226 221 225 eqtrd 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) = ( seq M ( + , F ) ` j ) )
227 193 fveq1i 
 |-  ( seq M ( + , F ) ` j ) = ( G ` j )
228 227 a1i 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( seq M ( + , F ) ` j ) = ( G ` j ) )
229 simp3 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( G ` j ) = z )
230 226 228 229 3eqtrrd 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> z = ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) )
231 61 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( sum^ ` F ) = ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) )
232 230 231 breq12d 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> ( z <_ ( sum^ ` F ) <-> ( sum^ ` ( k e. ( M ... j ) |-> ( F ` k ) ) ) <_ ( sum^ ` ( k e. Z |-> ( F ` k ) ) ) ) )
233 217 232 mpbird 
 |-  ( ( ph /\ j e. Z /\ ( G ` j ) = z ) -> z <_ ( sum^ ` F ) )
234 233 3exp 
 |-  ( ph -> ( j e. Z -> ( ( G ` j ) = z -> z <_ ( sum^ ` F ) ) ) )
235 234 adantr 
 |-  ( ( ph /\ z e. ran G ) -> ( j e. Z -> ( ( G ` j ) = z -> z <_ ( sum^ ` F ) ) ) )
236 235 rexlimdv 
 |-  ( ( ph /\ z e. ran G ) -> ( E. j e. Z ( G ` j ) = z -> z <_ ( sum^ ` F ) ) )
237 106 236 mpd 
 |-  ( ( ph /\ z e. ran G ) -> z <_ ( sum^ ` F ) )
238 237 ralrimiva 
 |-  ( ph -> A. z e. ran G z <_ ( sum^ ` F ) )
239 7 10 sge0cl 
 |-  ( ph -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
240 58 ltpnfd 
 |-  ( ph -> sup ( ran G , RR , < ) < +oo )
241 11 59 90 213 240 xrlelttrd 
 |-  ( ph -> ( sum^ ` F ) < +oo )
242 11 90 241 xrgtned 
 |-  ( ph -> +oo =/= ( sum^ ` F ) )
243 242 necomd 
 |-  ( ph -> ( sum^ ` F ) =/= +oo )
244 ge0xrre 
 |-  ( ( ( sum^ ` F ) e. ( 0 [,] +oo ) /\ ( sum^ ` F ) =/= +oo ) -> ( sum^ ` F ) e. RR )
245 239 243 244 syl2anc 
 |-  ( ph -> ( sum^ ` F ) e. RR )
246 suprleub 
 |-  ( ( ( ran G C_ RR /\ ran G =/= (/) /\ E. x e. RR A. z e. ran G z <_ x ) /\ ( sum^ ` F ) e. RR ) -> ( sup ( ran G , RR , < ) <_ ( sum^ ` F ) <-> A. z e. ran G z <_ ( sum^ ` F ) ) )
247 77 100 130 245 246 syl31anc 
 |-  ( ph -> ( sup ( ran G , RR , < ) <_ ( sum^ ` F ) <-> A. z e. ran G z <_ ( sum^ ` F ) ) )
248 238 247 mpbird 
 |-  ( ph -> sup ( ran G , RR , < ) <_ ( sum^ ` F ) )
249 11 59 213 248 xrletrid 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran G , RR , < ) )
250 climuni 
 |-  ( ( G ~~> B /\ G ~~> sup ( ran G , RR , < ) ) -> B = sup ( ran G , RR , < ) )
251 5 57 250 syl2anc 
 |-  ( ph -> B = sup ( ran G , RR , < ) )
252 249 251 eqtr4d 
 |-  ( ph -> ( sum^ ` F ) = B )