Metamath Proof Explorer

Theorem esumcvg

Description: The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 . (Contributed by Thierry Arnoux, 5-Sep-2017)

Ref Expression
Hypotheses esumcvg.j 
|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
esumcvg.f 
|- F = ( n e. NN |-> sum* k e. ( 1 ... n ) A )
esumcvg.a 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
esumcvg.m 
|- ( k = m -> A = B )
Assertion esumcvg 
|- ( ph -> F ( ~~>t ` J ) sum* k e. NN A )

Proof

Step Hyp Ref Expression
1 esumcvg.j 
 |-  J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2 esumcvg.f 
 |-  F = ( n e. NN |-> sum* k e. ( 1 ... n ) A )
3 esumcvg.a 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
4 esumcvg.m 
 |-  ( k = m -> A = B )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 1zzd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> 1 e. ZZ )
7 simpr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F e. dom ~~> )
8 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
9 ax-resscn 
 |-  RR C_ CC
10 8 9 sstri 
 |-  ( 0 [,) +oo ) C_ CC
11 4 eleq1d 
 |-  ( k = m -> ( A e. ( 0 [,) +oo ) <-> B e. ( 0 [,) +oo ) ) )
12 11 cbvralvw 
 |-  ( A. k e. NN A e. ( 0 [,) +oo ) <-> A. m e. NN B e. ( 0 [,) +oo ) )
13 rsp 
 |-  ( A. k e. NN A e. ( 0 [,) +oo ) -> ( k e. NN -> A e. ( 0 [,) +oo ) ) )
14 12 13 sylbir 
 |-  ( A. m e. NN B e. ( 0 [,) +oo ) -> ( k e. NN -> A e. ( 0 [,) +oo ) ) )
15 14 adantl 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> ( k e. NN -> A e. ( 0 [,) +oo ) ) )
16 15 imp 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
17 10 16 sselid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ k e. NN ) -> A e. CC )
18 17 adantlr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> A e. CC )
19 fzfid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> ( 1 ... n ) e. Fin )
20 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
21 20 16 sylan2 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,) +oo ) )
22 21 adantlr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,) +oo ) )
23 19 22 esumpfinval 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) A = sum_ k e. ( 1 ... n ) A )
24 23 mpteq2dva 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> ( n e. NN |-> sum* k e. ( 1 ... n ) A ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) )
25 2 24 eqtrid 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> F = ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) )
26 10 22 sselid 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. CC )
27 19 26 fsumcl 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A e. CC )
28 25 27 fvmpt2d 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> ( F ` n ) = sum_ k e. ( 1 ... n ) A )
29 28 adantlr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ n e. NN ) -> ( F ` n ) = sum_ k e. ( 1 ... n ) A )
30 5 6 7 18 29 isumclim3 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F ~~> sum_ k e. NN A )
31 19 22 fsumrp0cl 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A e. ( 0 [,) +oo ) )
32 23 31 eqeltrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,) +oo ) )
33 32 2 fmptd 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> F : NN --> ( 0 [,) +oo ) )
34 33 adantr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F : NN --> ( 0 [,) +oo ) )
35 simplll 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> ph )
36 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( m e. NN |-> B ) = ( m e. NN |-> B ) )
37 eqcom 
 |-  ( k = m <-> m = k )
38 eqcom 
 |-  ( A = B <-> B = A )
39 4 37 38 3imtr3i 
 |-  ( m = k -> B = A )
40 39 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ m = k ) -> B = A )
41 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
42 36 40 41 3 fvmptd 
 |-  ( ( ph /\ k e. NN ) -> ( ( m e. NN |-> B ) ` k ) = A )
43 35 42 sylancom 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> ( ( m e. NN |-> B ) ` k ) = A )
44 16 adantlr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
45 elrege0 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
46 44 45 sylib 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> ( A e. RR /\ 0 <_ A ) )
47 46 simpld 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> A e. RR )
48 ovex 
 |-  ( 1 ... n ) e. _V
49 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
50 20 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
51 49 50 3 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,] +oo ) )
52 51 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
53 nfcv 
 |-  F/_ k ( 1 ... n )
54 53 esumcl 
 |-  ( ( ( 1 ... n ) e. _V /\ A. k e. ( 1 ... n ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
55 48 52 54 sylancr 
 |-  ( ( ph /\ n e. NN ) -> sum* k e. ( 1 ... n ) A e. ( 0 [,] +oo ) )
56 55 2 fmptd 
 |-  ( ph -> F : NN --> ( 0 [,] +oo ) )
57 56 ffnd 
 |-  ( ph -> F Fn NN )
58 57 adantr 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> F Fn NN )
59 1z 
 |-  1 e. ZZ
60 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( m e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) )
61 59 60 ax-mp 
 |-  seq 1 ( + , ( m e. NN |-> B ) ) Fn ( ZZ>= ` 1 )
62 5 fneq2i 
 |-  ( seq 1 ( + , ( m e. NN |-> B ) ) Fn NN <-> seq 1 ( + , ( m e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) )
63 61 62 mpbir 
 |-  seq 1 ( + , ( m e. NN |-> B ) ) Fn NN
64 63 a1i 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> seq 1 ( + , ( m e. NN |-> B ) ) Fn NN )
65 simplll 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
66 20 42 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... n ) ) -> ( ( m e. NN |-> B ) ` k ) = A )
67 65 66 sylancom 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( m e. NN |-> B ) ` k ) = A )
68 simpr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> n e. NN )
69 68 5 eleqtrdi 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
70 67 69 26 fsumser 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A = ( seq 1 ( + , ( m e. NN |-> B ) ) ` n ) )
71 28 70 eqtrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> ( F ` n ) = ( seq 1 ( + , ( m e. NN |-> B ) ) ` n ) )
72 58 64 71 eqfnfvd 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> F = seq 1 ( + , ( m e. NN |-> B ) ) )
73 72 adantr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F = seq 1 ( + , ( m e. NN |-> B ) ) )
74 73 7 eqeltrrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> seq 1 ( + , ( m e. NN |-> B ) ) e. dom ~~> )
75 5 6 43 47 74 isumrecl 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> sum_ k e. NN A e. RR )
76 46 simprd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) /\ k e. NN ) -> 0 <_ A )
77 5 6 43 47 74 76 isumge0 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> 0 <_ sum_ k e. NN A )
78 elrege0 
 |-  ( sum_ k e. NN A e. ( 0 [,) +oo ) <-> ( sum_ k e. NN A e. RR /\ 0 <_ sum_ k e. NN A ) )
79 75 77 78 sylanbrc 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> sum_ k e. NN A e. ( 0 [,) +oo ) )
80 ssid 
 |-  ( 0 [,) +oo ) C_ ( 0 [,) +oo )
81 1 34 79 80 lmlimxrge0 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> ( F ( ~~>t ` J ) sum_ k e. NN A <-> F ~~> sum_ k e. NN A ) )
82 30 81 mpbird 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F ( ~~>t ` J ) sum_ k e. NN A )
83 2 7 eqeltrrid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> ( n e. NN |-> sum* k e. ( 1 ... n ) A ) e. dom ~~> )
84 24 eleq1d 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) e. dom ~~> <-> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> ) )
85 84 adantr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) e. dom ~~> <-> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> ) )
86 83 85 mpbid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> )
87 44 4 86 esumpcvgval 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> sum* k e. NN A = sum_ k e. NN A )
88 82 87 breqtrrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ F e. dom ~~> ) -> F ( ~~>t ` J ) sum* k e. NN A )
89 33 adantr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> F : NN --> ( 0 [,) +oo ) )
90 simpr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> n e. NN )
91 90 nnzd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> n e. ZZ )
92 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
93 peano2uz 
 |-  ( n e. ( ZZ>= ` n ) -> ( n + 1 ) e. ( ZZ>= ` n ) )
94 91 92 93 3syl 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> ( n + 1 ) e. ( ZZ>= ` n ) )
95 simplll 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ k e. NN ) -> ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) )
96 95 16 sylancom 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
97 90 94 96 esumpmono 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> sum* k e. ( 1 ... n ) A <_ sum* k e. ( 1 ... ( n + 1 ) ) A )
98 28 23 eqtr4d 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ n e. NN ) -> ( F ` n ) = sum* k e. ( 1 ... n ) A )
99 98 adantlr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> ( F ` n ) = sum* k e. ( 1 ... n ) A )
100 oveq2 
 |-  ( l = n -> ( 1 ... l ) = ( 1 ... n ) )
101 esumeq1 
 |-  ( ( 1 ... l ) = ( 1 ... n ) -> sum* k e. ( 1 ... l ) A = sum* k e. ( 1 ... n ) A )
102 100 101 syl 
 |-  ( l = n -> sum* k e. ( 1 ... l ) A = sum* k e. ( 1 ... n ) A )
103 102 cbvmptv 
 |-  ( l e. NN |-> sum* k e. ( 1 ... l ) A ) = ( n e. NN |-> sum* k e. ( 1 ... n ) A )
104 2 103 eqtr4i 
 |-  F = ( l e. NN |-> sum* k e. ( 1 ... l ) A )
105 104 a1i 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> F = ( l e. NN |-> sum* k e. ( 1 ... l ) A ) )
106 simpr3 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ ( -. F e. dom ~~> /\ n e. NN /\ l = ( n + 1 ) ) ) -> l = ( n + 1 ) )
107 oveq2 
 |-  ( l = ( n + 1 ) -> ( 1 ... l ) = ( 1 ... ( n + 1 ) ) )
108 esumeq1 
 |-  ( ( 1 ... l ) = ( 1 ... ( n + 1 ) ) -> sum* k e. ( 1 ... l ) A = sum* k e. ( 1 ... ( n + 1 ) ) A )
109 106 107 108 3syl 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ ( -. F e. dom ~~> /\ n e. NN /\ l = ( n + 1 ) ) ) -> sum* k e. ( 1 ... l ) A = sum* k e. ( 1 ... ( n + 1 ) ) A )
110 109 3anassrs 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ l = ( n + 1 ) ) -> sum* k e. ( 1 ... l ) A = sum* k e. ( 1 ... ( n + 1 ) ) A )
111 90 peano2nnd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> ( n + 1 ) e. NN )
112 ovex 
 |-  ( 1 ... ( n + 1 ) ) e. _V
113 simp-4l 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ k e. ( 1 ... ( n + 1 ) ) ) -> ph )
114 elfznn 
 |-  ( k e. ( 1 ... ( n + 1 ) ) -> k e. NN )
115 114 adantl 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ k e. ( 1 ... ( n + 1 ) ) ) -> k e. NN )
116 113 115 3 syl2anc 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) /\ k e. ( 1 ... ( n + 1 ) ) ) -> A e. ( 0 [,] +oo ) )
117 116 ralrimiva 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> A. k e. ( 1 ... ( n + 1 ) ) A e. ( 0 [,] +oo ) )
118 nfcv 
 |-  F/_ k ( 1 ... ( n + 1 ) )
119 118 esumcl 
 |-  ( ( ( 1 ... ( n + 1 ) ) e. _V /\ A. k e. ( 1 ... ( n + 1 ) ) A e. ( 0 [,] +oo ) ) -> sum* k e. ( 1 ... ( n + 1 ) ) A e. ( 0 [,] +oo ) )
120 112 117 119 sylancr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> sum* k e. ( 1 ... ( n + 1 ) ) A e. ( 0 [,] +oo ) )
121 105 110 111 120 fvmptd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> ( F ` ( n + 1 ) ) = sum* k e. ( 1 ... ( n + 1 ) ) A )
122 97 99 121 3brtr4d 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ n e. NN ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
123 simpr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> -. F e. dom ~~> )
124 1 89 122 123 lmdvglim 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> F ( ~~>t ` J ) +oo )
125 nfv 
 |-  F/ k ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) )
126 nfcv 
 |-  F/_ k NN
127 nnex 
 |-  NN e. _V
128 127 a1i 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> NN e. _V )
129 3 adantlr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
130 simpr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> x e. ( ~P NN i^i Fin ) )
131 simpll 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) )
132 inss1 
 |-  ( ~P NN i^i Fin ) C_ ~P NN
133 simplr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> x e. ( ~P NN i^i Fin ) )
134 132 133 sselid 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> x e. ~P NN )
135 134 elpwid 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> x C_ NN )
136 simpr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> k e. x )
137 135 136 sseldd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> k e. NN )
138 131 137 16 syl2anc 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> A e. ( 0 [,) +oo ) )
139 138 fmpttd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> ( k e. x |-> A ) : x --> ( 0 [,) +oo ) )
140 esumpfinvallem 
 |-  ( ( x e. ( ~P NN i^i Fin ) /\ ( k e. x |-> A ) : x --> ( 0 [,) +oo ) ) -> ( CCfld gsum ( k e. x |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> A ) ) )
141 130 139 140 syl2anc 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. x |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> A ) ) )
142 inss2 
 |-  ( ~P NN i^i Fin ) C_ Fin
143 142 130 sselid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> x e. Fin )
144 131 137 17 syl2anc 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> A e. CC )
145 143 144 gsumfsum 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. x |-> A ) ) = sum_ k e. x A )
146 141 145 eqtr3d 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ x e. ( ~P NN i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> A ) ) = sum_ k e. x A )
147 125 126 128 129 146 esumval 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> sum* k e. NN A = sup ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) , RR* , < ) )
148 147 adantr 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> sum* k e. NN A = sup ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) , RR* , < ) )
149 89 122 123 lmdvg 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> A. y e. RR E. l e. NN A. n e. ( ZZ>= ` l ) y < ( F ` n ) )
150 149 r19.21bi 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) -> E. l e. NN A. n e. ( ZZ>= ` l ) y < ( F ` n ) )
151 nnz 
 |-  ( l e. NN -> l e. ZZ )
152 uzid 
 |-  ( l e. ZZ -> l e. ( ZZ>= ` l ) )
153 151 152 syl 
 |-  ( l e. NN -> l e. ( ZZ>= ` l ) )
154 simpr 
 |-  ( ( l e. NN /\ n = l ) -> n = l )
155 154 fveq2d 
 |-  ( ( l e. NN /\ n = l ) -> ( F ` n ) = ( F ` l ) )
156 155 breq2d 
 |-  ( ( l e. NN /\ n = l ) -> ( y < ( F ` n ) <-> y < ( F ` l ) ) )
157 153 156 rspcdv 
 |-  ( l e. NN -> ( A. n e. ( ZZ>= ` l ) y < ( F ` n ) -> y < ( F ` l ) ) )
158 157 reximia 
 |-  ( E. l e. NN A. n e. ( ZZ>= ` l ) y < ( F ` n ) -> E. l e. NN y < ( F ` l ) )
159 150 158 syl 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) -> E. l e. NN y < ( F ` l ) )
160 simplr 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> y e. RR )
161 89 ad2antrr 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> F : NN --> ( 0 [,) +oo ) )
162 simpr 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> l e. NN )
163 161 162 ffvelrnd 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( F ` l ) e. ( 0 [,) +oo ) )
164 8 163 sselid 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( F ` l ) e. RR )
165 ltle 
 |-  ( ( y e. RR /\ ( F ` l ) e. RR ) -> ( y < ( F ` l ) -> y <_ ( F ` l ) ) )
166 160 164 165 syl2anc 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( y < ( F ` l ) -> y <_ ( F ` l ) ) )
167 oveq2 
 |-  ( n = l -> ( 1 ... n ) = ( 1 ... l ) )
168 esumeq1 
 |-  ( ( 1 ... n ) = ( 1 ... l ) -> sum* k e. ( 1 ... n ) A = sum* k e. ( 1 ... l ) A )
169 167 168 syl 
 |-  ( n = l -> sum* k e. ( 1 ... n ) A = sum* k e. ( 1 ... l ) A )
170 esumex 
 |-  sum* k e. ( 1 ... l ) A e. _V
171 170 a1i 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> sum* k e. ( 1 ... l ) A e. _V )
172 2 169 162 171 fvmptd3 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( F ` l ) = sum* k e. ( 1 ... l ) A )
173 fzfid 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( 1 ... l ) e. Fin )
174 simp-4l 
 |-  ( ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) /\ k e. ( 1 ... l ) ) -> ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) )
175 elfznn 
 |-  ( k e. ( 1 ... l ) -> k e. NN )
176 175 adantl 
 |-  ( ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) /\ k e. ( 1 ... l ) ) -> k e. NN )
177 174 176 16 syl2anc 
 |-  ( ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) /\ k e. ( 1 ... l ) ) -> A e. ( 0 [,) +oo ) )
178 173 177 esumpfinval 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> sum* k e. ( 1 ... l ) A = sum_ k e. ( 1 ... l ) A )
179 172 178 eqtrd 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( F ` l ) = sum_ k e. ( 1 ... l ) A )
180 179 breq2d 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( y <_ ( F ` l ) <-> y <_ sum_ k e. ( 1 ... l ) A ) )
181 166 180 sylibd 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) /\ l e. NN ) -> ( y < ( F ` l ) -> y <_ sum_ k e. ( 1 ... l ) A ) )
182 181 reximdva 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) -> ( E. l e. NN y < ( F ` l ) -> E. l e. NN y <_ sum_ k e. ( 1 ... l ) A ) )
183 159 182 mpd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) -> E. l e. NN y <_ sum_ k e. ( 1 ... l ) A )
184 fzssuz 
 |-  ( 1 ... l ) C_ ( ZZ>= ` 1 )
185 184 5 sseqtrri 
 |-  ( 1 ... l ) C_ NN
186 ovex 
 |-  ( 1 ... l ) e. _V
187 186 elpw 
 |-  ( ( 1 ... l ) e. ~P NN <-> ( 1 ... l ) C_ NN )
188 185 187 mpbir 
 |-  ( 1 ... l ) e. ~P NN
189 fzfi 
 |-  ( 1 ... l ) e. Fin
190 elin 
 |-  ( ( 1 ... l ) e. ( ~P NN i^i Fin ) <-> ( ( 1 ... l ) e. ~P NN /\ ( 1 ... l ) e. Fin ) )
191 188 189 190 mpbir2an 
 |-  ( 1 ... l ) e. ( ~P NN i^i Fin )
192 sumex 
 |-  sum_ k e. ( 1 ... l ) A e. _V
193 eqid 
 |-  ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) = ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A )
194 sumeq1 
 |-  ( x = ( 1 ... l ) -> sum_ k e. x A = sum_ k e. ( 1 ... l ) A )
195 193 194 elrnmpt1s 
 |-  ( ( ( 1 ... l ) e. ( ~P NN i^i Fin ) /\ sum_ k e. ( 1 ... l ) A e. _V ) -> sum_ k e. ( 1 ... l ) A e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) )
196 191 192 195 mp2an 
 |-  sum_ k e. ( 1 ... l ) A e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A )
197 nfv 
 |-  F/ z y <_ sum_ k e. ( 1 ... l ) A
198 breq2 
 |-  ( z = sum_ k e. ( 1 ... l ) A -> ( y <_ z <-> y <_ sum_ k e. ( 1 ... l ) A ) )
199 197 198 rspce 
 |-  ( ( sum_ k e. ( 1 ... l ) A e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) /\ y <_ sum_ k e. ( 1 ... l ) A ) -> E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z )
200 196 199 mpan 
 |-  ( y <_ sum_ k e. ( 1 ... l ) A -> E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z )
201 200 rexlimivw 
 |-  ( E. l e. NN y <_ sum_ k e. ( 1 ... l ) A -> E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z )
202 183 201 syl 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ y e. RR ) -> E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z )
203 202 ralrimiva 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> A. y e. RR E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z )
204 simpr 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) -> x e. ( ~P NN i^i Fin ) )
205 142 204 sselid 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) -> x e. Fin )
206 138 adantllr 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> A e. ( 0 [,) +oo ) )
207 8 206 sselid 
 |-  ( ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) /\ k e. x ) -> A e. RR )
208 205 207 fsumrecl 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) -> sum_ k e. x A e. RR )
209 208 rexrd 
 |-  ( ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) /\ x e. ( ~P NN i^i Fin ) ) -> sum_ k e. x A e. RR* )
210 209 fmpttd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) : ( ~P NN i^i Fin ) --> RR* )
211 frn 
 |-  ( ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) : ( ~P NN i^i Fin ) --> RR* -> ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) C_ RR* )
212 supxrunb1 
 |-  ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) C_ RR* -> ( A. y e. RR E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z <-> sup ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) , RR* , < ) = +oo ) )
213 210 211 212 3syl 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> ( A. y e. RR E. z e. ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) y <_ z <-> sup ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) , RR* , < ) = +oo ) )
214 203 213 mpbid 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> sup ( ran ( x e. ( ~P NN i^i Fin ) |-> sum_ k e. x A ) , RR* , < ) = +oo )
215 148 214 eqtrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> sum* k e. NN A = +oo )
216 124 215 breqtrrd 
 |-  ( ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) /\ -. F e. dom ~~> ) -> F ( ~~>t ` J ) sum* k e. NN A )
217 88 216 pm2.61dan 
 |-  ( ( ph /\ A. m e. NN B e. ( 0 [,) +oo ) ) -> F ( ~~>t ` J ) sum* k e. NN A )
218 2 reseq1i 
 |-  ( F |` ( ZZ>= ` k ) ) = ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` k ) )
219 eleq1w 
 |-  ( l = k -> ( l e. NN <-> k e. NN ) )
220 219 anbi2d 
 |-  ( l = k -> ( ( ph /\ l e. NN ) <-> ( ph /\ k e. NN ) ) )
221 sbequ12r 
 |-  ( l = k -> ( [ l / k ] A = +oo <-> A = +oo ) )
222 220 221 anbi12d 
 |-  ( l = k -> ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) <-> ( ( ph /\ k e. NN ) /\ A = +oo ) ) )
223 fveq2 
 |-  ( l = k -> ( ZZ>= ` l ) = ( ZZ>= ` k ) )
224 223 reseq2d 
 |-  ( l = k -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` k ) ) )
225 223 xpeq1d 
 |-  ( l = k -> ( ( ZZ>= ` l ) X. { +oo } ) = ( ( ZZ>= ` k ) X. { +oo } ) )
226 224 225 eqeq12d 
 |-  ( l = k -> ( ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( ( ZZ>= ` l ) X. { +oo } ) <-> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) )
227 222 226 imbi12d 
 |-  ( l = k -> ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( ( ZZ>= ` l ) X. { +oo } ) ) <-> ( ( ( ph /\ k e. NN ) /\ A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) ) )
228 nfv 
 |-  F/ k ( ph /\ l e. NN )
229 nfs1v 
 |-  F/ k [ l / k ] A = +oo
230 228 229 nfan 
 |-  F/ k ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo )
231 nfv 
 |-  F/ k n e. ( ZZ>= ` l )
232 230 231 nfan 
 |-  F/ k ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) )
233 ovexd 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> ( 1 ... n ) e. _V )
234 simp-4l 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) /\ k e. ( 1 ... n ) ) -> ph )
235 20 adantl 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) /\ k e. ( 1 ... n ) ) -> k e. NN )
236 234 235 3 syl2anc 
 |-  ( ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) /\ k e. ( 1 ... n ) ) -> A e. ( 0 [,] +oo ) )
237 simpllr 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> l e. NN )
238 elnnuz 
 |-  ( l e. NN <-> l e. ( ZZ>= ` 1 ) )
239 eluzfz 
 |-  ( ( l e. ( ZZ>= ` 1 ) /\ n e. ( ZZ>= ` l ) ) -> l e. ( 1 ... n ) )
240 238 239 sylanb 
 |-  ( ( l e. NN /\ n e. ( ZZ>= ` l ) ) -> l e. ( 1 ... n ) )
241 237 240 sylancom 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> l e. ( 1 ... n ) )
242 simplr 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> [ l / k ] A = +oo )
243 sbequ12 
 |-  ( k = l -> ( A = +oo <-> [ l / k ] A = +oo ) )
244 229 243 rspce 
 |-  ( ( l e. ( 1 ... n ) /\ [ l / k ] A = +oo ) -> E. k e. ( 1 ... n ) A = +oo )
245 241 242 244 syl2anc 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> E. k e. ( 1 ... n ) A = +oo )
246 232 233 236 245 esumpinfval 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ n e. ( ZZ>= ` l ) ) -> sum* k e. ( 1 ... n ) A = +oo )
247 246 ralrimiva 
 |-  ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo )
248 eqidd 
 |-  ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> ( ZZ>= ` l ) = ( ZZ>= ` l ) )
249 mpteq12 
 |-  ( ( ( ZZ>= ` l ) = ( ZZ>= ` l ) /\ A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo ) -> ( n e. ( ZZ>= ` l ) |-> sum* k e. ( 1 ... n ) A ) = ( n e. ( ZZ>= ` l ) |-> +oo ) )
250 248 249 sylan 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo ) -> ( n e. ( ZZ>= ` l ) |-> sum* k e. ( 1 ... n ) A ) = ( n e. ( ZZ>= ` l ) |-> +oo ) )
251 simplr 
 |-  ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> l e. NN )
252 uznnssnn 
 |-  ( l e. NN -> ( ZZ>= ` l ) C_ NN )
253 resmpt 
 |-  ( ( ZZ>= ` l ) C_ NN -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( n e. ( ZZ>= ` l ) |-> sum* k e. ( 1 ... n ) A ) )
254 251 252 253 3syl 
 |-  ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( n e. ( ZZ>= ` l ) |-> sum* k e. ( 1 ... n ) A ) )
255 254 adantr 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( n e. ( ZZ>= ` l ) |-> sum* k e. ( 1 ... n ) A ) )
256 fconstmpt 
 |-  ( ( ZZ>= ` l ) X. { +oo } ) = ( n e. ( ZZ>= ` l ) |-> +oo )
257 256 a1i 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo ) -> ( ( ZZ>= ` l ) X. { +oo } ) = ( n e. ( ZZ>= ` l ) |-> +oo ) )
258 250 255 257 3eqtr4d 
 |-  ( ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) /\ A. n e. ( ZZ>= ` l ) sum* k e. ( 1 ... n ) A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( ( ZZ>= ` l ) X. { +oo } ) )
259 247 258 mpdan 
 |-  ( ( ( ph /\ l e. NN ) /\ [ l / k ] A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` l ) ) = ( ( ZZ>= ` l ) X. { +oo } ) )
260 227 259 chvarvv 
 |-  ( ( ( ph /\ k e. NN ) /\ A = +oo ) -> ( ( n e. NN |-> sum* k e. ( 1 ... n ) A ) |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) )
261 218 260 eqtrid 
 |-  ( ( ( ph /\ k e. NN ) /\ A = +oo ) -> ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) )
262 261 ex 
 |-  ( ( ph /\ k e. NN ) -> ( A = +oo -> ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) )
263 262 reximdva 
 |-  ( ph -> ( E. k e. NN A = +oo -> E. k e. NN ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) )
264 263 imp 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> E. k e. NN ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) )
265 xrge0topn 
 |-  ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
266 1 265 eqtri 
 |-  J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
267 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
268 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
269 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) )
270 267 268 269 mp2an 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) )
271 266 270 eqeltri 
 |-  J e. ( TopOn ` ( 0 [,] +oo ) )
272 271 a1i 
 |-  ( ( ph /\ k e. NN ) -> J e. ( TopOn ` ( 0 [,] +oo ) ) )
273 0xr 
 |-  0 e. RR*
274 pnfxr 
 |-  +oo e. RR*
275 0lepnf 
 |-  0 <_ +oo
276 ubicc2 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
277 273 274 275 276 mp3an 
 |-  +oo e. ( 0 [,] +oo )
278 277 a1i 
 |-  ( ( ph /\ k e. NN ) -> +oo e. ( 0 [,] +oo ) )
279 41 nnzd 
 |-  ( ( ph /\ k e. NN ) -> k e. ZZ )
280 eqid 
 |-  ( ZZ>= ` k ) = ( ZZ>= ` k )
281 280 lmconst 
 |-  ( ( J e. ( TopOn ` ( 0 [,] +oo ) ) /\ +oo e. ( 0 [,] +oo ) /\ k e. ZZ ) -> ( ( ZZ>= ` k ) X. { +oo } ) ( ~~>t ` J ) +oo )
282 272 278 279 281 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( ZZ>= ` k ) X. { +oo } ) ( ~~>t ` J ) +oo )
283 breq1 
 |-  ( ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) -> ( ( F |` ( ZZ>= ` k ) ) ( ~~>t ` J ) +oo <-> ( ( ZZ>= ` k ) X. { +oo } ) ( ~~>t ` J ) +oo ) )
284 283 biimprd 
 |-  ( ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) -> ( ( ( ZZ>= ` k ) X. { +oo } ) ( ~~>t ` J ) +oo -> ( F |` ( ZZ>= ` k ) ) ( ~~>t ` J ) +oo ) )
285 282 284 mpan9 
 |-  ( ( ( ph /\ k e. NN ) /\ ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) -> ( F |` ( ZZ>= ` k ) ) ( ~~>t ` J ) +oo )
286 ovexd 
 |-  ( ( ph /\ k e. NN ) -> ( 0 [,] +oo ) e. _V )
287 cnex 
 |-  CC e. _V
288 287 a1i 
 |-  ( ( ph /\ k e. NN ) -> CC e. _V )
289 56 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : NN --> ( 0 [,] +oo ) )
290 nnsscn 
 |-  NN C_ CC
291 290 a1i 
 |-  ( ( ph /\ k e. NN ) -> NN C_ CC )
292 elpm2r 
 |-  ( ( ( ( 0 [,] +oo ) e. _V /\ CC e. _V ) /\ ( F : NN --> ( 0 [,] +oo ) /\ NN C_ CC ) ) -> F e. ( ( 0 [,] +oo ) ^pm CC ) )
293 286 288 289 291 292 syl22anc 
 |-  ( ( ph /\ k e. NN ) -> F e. ( ( 0 [,] +oo ) ^pm CC ) )
294 272 293 279 lmres 
 |-  ( ( ph /\ k e. NN ) -> ( F ( ~~>t ` J ) +oo <-> ( F |` ( ZZ>= ` k ) ) ( ~~>t ` J ) +oo ) )
295 294 biimpar 
 |-  ( ( ( ph /\ k e. NN ) /\ ( F |` ( ZZ>= ` k ) ) ( ~~>t ` J ) +oo ) -> F ( ~~>t ` J ) +oo )
296 285 295 syldan 
 |-  ( ( ( ph /\ k e. NN ) /\ ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) -> F ( ~~>t ` J ) +oo )
297 296 r19.29an 
 |-  ( ( ph /\ E. k e. NN ( F |` ( ZZ>= ` k ) ) = ( ( ZZ>= ` k ) X. { +oo } ) ) -> F ( ~~>t ` J ) +oo )
298 264 297 syldan 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> F ( ~~>t ` J ) +oo )
299 nfv 
 |-  F/ k ph
300 nfre1 
 |-  F/ k E. k e. NN A = +oo
301 299 300 nfan 
 |-  F/ k ( ph /\ E. k e. NN A = +oo )
302 127 a1i 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> NN e. _V )
303 3 adantlr 
 |-  ( ( ( ph /\ E. k e. NN A = +oo ) /\ k e. NN ) -> A e. ( 0 [,] +oo ) )
304 simpr 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> E. k e. NN A = +oo )
305 301 302 303 304 esumpinfval 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> sum* k e. NN A = +oo )
306 298 305 breqtrrd 
 |-  ( ( ph /\ E. k e. NN A = +oo ) -> F ( ~~>t ` J ) sum* k e. NN A )
307 eleq1w 
 |-  ( k = m -> ( k e. NN <-> m e. NN ) )
308 307 anbi2d 
 |-  ( k = m -> ( ( ph /\ k e. NN ) <-> ( ph /\ m e. NN ) ) )
309 4 eleq1d 
 |-  ( k = m -> ( A e. ( 0 [,] +oo ) <-> B e. ( 0 [,] +oo ) ) )
310 308 309 imbi12d 
 |-  ( k = m -> ( ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) ) <-> ( ( ph /\ m e. NN ) -> B e. ( 0 [,] +oo ) ) ) )
311 310 3 chvarvv 
 |-  ( ( ph /\ m e. NN ) -> B e. ( 0 [,] +oo ) )
312 eliccelico 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> ( B e. ( 0 [,] +oo ) <-> ( B e. ( 0 [,) +oo ) \/ B = +oo ) ) )
313 273 274 275 312 mp3an 
 |-  ( B e. ( 0 [,] +oo ) <-> ( B e. ( 0 [,) +oo ) \/ B = +oo ) )
314 311 313 sylib 
 |-  ( ( ph /\ m e. NN ) -> ( B e. ( 0 [,) +oo ) \/ B = +oo ) )
315 314 ralrimiva 
 |-  ( ph -> A. m e. NN ( B e. ( 0 [,) +oo ) \/ B = +oo ) )
316 r19.30 
 |-  ( A. m e. NN ( B e. ( 0 [,) +oo ) \/ B = +oo ) -> ( A. m e. NN B e. ( 0 [,) +oo ) \/ E. m e. NN B = +oo ) )
317 315 316 syl 
 |-  ( ph -> ( A. m e. NN B e. ( 0 [,) +oo ) \/ E. m e. NN B = +oo ) )
318 4 eqeq1d 
 |-  ( k = m -> ( A = +oo <-> B = +oo ) )
319 318 cbvrexvw 
 |-  ( E. k e. NN A = +oo <-> E. m e. NN B = +oo )
320 319 orbi2i 
 |-  ( ( A. m e. NN B e. ( 0 [,) +oo ) \/ E. k e. NN A = +oo ) <-> ( A. m e. NN B e. ( 0 [,) +oo ) \/ E. m e. NN B = +oo ) )
321 317 320 sylibr 
 |-  ( ph -> ( A. m e. NN B e. ( 0 [,) +oo ) \/ E. k e. NN A = +oo ) )
322 217 306 321 mpjaodan 
 |-  ( ph -> F ( ~~>t ` J ) sum* k e. NN A )