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