Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumcvg Structured version   Unicode version

Theorem esumcvg 28315
Description: The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 13631. (Contributed by Thierry Arnoux, 5-Sep-2017.)
Hypotheses
Ref Expression
esumcvg.j  |-  J  =  ( TopOpen `  ( RR*ss  ( 0 [,] +oo ) ) )
esumcvg.f  |-  F  =  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )
esumcvg.a  |-  ( (
ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
esumcvg.m  |-  ( k  =  m  ->  A  =  B )
Assertion
Ref Expression
esumcvg  |-  ( ph  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
Distinct variable groups:    m, n, A    k, n, B    k, m, F, n    k, J, n    ph, k, m, n
Allowed substitution hints:    A( k)    B( m)    J( m)

Proof of Theorem esumcvg
Dummy variables  l  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11117 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10891 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  1  e.  ZZ )
3 simpr 459 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F  e.  dom  ~~>  )
4 rge0ssre 11631 . . . . . . . . 9  |-  ( 0 [,) +oo )  C_  RR
5 ax-resscn 9538 . . . . . . . . 9  |-  RR  C_  CC
64, 5sstri 3498 . . . . . . . 8  |-  ( 0 [,) +oo )  C_  CC
7 esumcvg.m . . . . . . . . . . . . 13  |-  ( k  =  m  ->  A  =  B )
87eleq1d 2523 . . . . . . . . . . . 12  |-  ( k  =  m  ->  ( A  e.  ( 0 [,) +oo )  <->  B  e.  ( 0 [,) +oo ) ) )
98cbvralv 3081 . . . . . . . . . . 11  |-  ( A. k  e.  NN  A  e.  ( 0 [,) +oo ) 
<-> 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )
10 rsp 2820 . . . . . . . . . . 11  |-  ( A. k  e.  NN  A  e.  ( 0 [,) +oo )  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
119, 10sylbir 213 . . . . . . . . . 10  |-  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
1211adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
1312imp 427 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  ( 0 [,) +oo ) )
146, 13sseldi 3487 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  CC )
1514adantlr 712 . . . . . 6  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  A  e.  CC )
16 esumcvg.f . . . . . . . . 9  |-  F  =  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )
17 fzfid 12065 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  (
1 ... n )  e. 
Fin )
18 elfznn 11717 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... n )  ->  k  e.  NN )
1918, 13sylan2 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,) +oo ) )
2019adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,) +oo ) )
2117, 20esumpfinval 28304 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  =  sum_ k  e.  ( 1 ... n
) A )
2221mpteq2dva 4525 . . . . . . . . 9  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  =  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n
) A ) )
2316, 22syl5eq 2507 . . . . . . . 8  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  =  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A ) )
246, 20sseldi 3487 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  CC )
2517, 24fsumcl 13637 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) A  e.  CC )
2623, 25fvmpt2d 5941 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  ( F `  n )  =  sum_ k  e.  ( 1 ... n ) A )
2726adantlr 712 . . . . . 6  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( F `  n )  =  sum_ k  e.  ( 1 ... n ) A )
281, 2, 3, 15, 27isumclim3 13656 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F  ~~>  sum_ k  e.  NN  A
)
29 esumcvg.j . . . . . 6  |-  J  =  ( TopOpen `  ( RR*ss  ( 0 [,] +oo ) ) )
3017, 20fsumrp0cl 27919 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) A  e.  ( 0 [,) +oo )
)
3121, 30eqeltrd 2542 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  e.  ( 0 [,) +oo ) )
3231, 16fmptd 6031 . . . . . . 7  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F : NN
--> ( 0 [,) +oo ) )
3332adantr 463 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F : NN --> ( 0 [,) +oo ) )
34 simplll 757 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  ph )
35 eqidd 2455 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( m  e.  NN  |->  B )  =  ( m  e.  NN  |->  B ) )
36 eqcom 2463 . . . . . . . . . . . 12  |-  ( k  =  m  <->  m  =  k )
37 eqcom 2463 . . . . . . . . . . . 12  |-  ( A  =  B  <->  B  =  A )
387, 36, 373imtr3i 265 . . . . . . . . . . 11  |-  ( m  =  k  ->  B  =  A )
3938adantl 464 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  =  k )  ->  B  =  A )
40 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
41 esumcvg.a . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
4235, 39, 40, 41fvmptd 5936 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( m  e.  NN  |->  B ) `  k )  =  A )
4334, 42sylancom 665 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  (
( m  e.  NN  |->  B ) `  k
)  =  A )
4413adantlr 712 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  A  e.  ( 0 [,) +oo ) )
45 elrege0 11630 . . . . . . . . . 10  |-  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) )
4644, 45sylib 196 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  ( A  e.  RR  /\  0  <_  A ) )
4746simpld 457 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  A  e.  RR )
48 ovex 6298 . . . . . . . . . . . . . . 15  |-  ( 1 ... n )  e. 
_V
49 simpll 751 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ph )
5018adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
5149, 50, 41syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,] +oo ) )
5251ralrimiva 2868 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  A. k  e.  ( 1 ... n
) A  e.  ( 0 [,] +oo )
)
53 nfcv 2616 . . . . . . . . . . . . . . . 16  |-  F/_ k
( 1 ... n
)
5453esumcl 28259 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... n
)  e.  _V  /\  A. k  e.  ( 1 ... n ) A  e.  ( 0 [,] +oo ) )  -> Σ* k  e.  ( 1 ... n ) A  e.  ( 0 [,] +oo ) )
5548, 52, 54sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  e.  ( 0 [,] +oo ) )
5655, 16fmptd 6031 . . . . . . . . . . . . 13  |-  ( ph  ->  F : NN --> ( 0 [,] +oo ) )
57 ffn 5713 . . . . . . . . . . . . 13  |-  ( F : NN --> ( 0 [,] +oo )  ->  F  Fn  NN )
5856, 57syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  F  Fn  NN )
5958adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  Fn  NN )
60 1z 10890 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
61 seqfn 12101 . . . . . . . . . . . . . 14  |-  ( 1  e.  ZZ  ->  seq 1 (  +  , 
( m  e.  NN  |->  B ) )  Fn  ( ZZ>= `  1 )
)
6260, 61ax-mp 5 . . . . . . . . . . . . 13  |-  seq 1
(  +  ,  ( m  e.  NN  |->  B ) )  Fn  ( ZZ>=
`  1 )
631fneq2i 5658 . . . . . . . . . . . . 13  |-  (  seq 1 (  +  , 
( m  e.  NN  |->  B ) )  Fn  NN  <->  seq 1 (  +  ,  ( m  e.  NN  |->  B ) )  Fn  ( ZZ>= `  1
) )
6462, 63mpbir 209 . . . . . . . . . . . 12  |-  seq 1
(  +  ,  ( m  e.  NN  |->  B ) )  Fn  NN
6564a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  seq 1
(  +  ,  ( m  e.  NN  |->  B ) )  Fn  NN )
66 simplll 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ph )
6718, 42sylan2 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 1 ... n
) )  ->  (
( m  e.  NN  |->  B ) `  k
)  =  A )
6866, 67sylancom 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  (
( m  e.  NN  |->  B ) `  k
)  =  A )
69 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  n  e.  NN )
7069, 1syl6eleq 2552 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
7168, 70, 24fsumser 13634 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
7226, 71eqtrd 2495 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  ( F `  n )  =  (  seq 1
(  +  ,  ( m  e.  NN  |->  B ) ) `  n
) )
7359, 65, 72eqfnfvd 5960 . . . . . . . . . 10  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  =  seq 1 (  +  , 
( m  e.  NN  |->  B ) ) )
7473adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F  =  seq 1 (  +  ,  ( m  e.  NN  |->  B ) ) )
7574, 3eqeltrrd 2543 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  seq 1 (  +  , 
( m  e.  NN  |->  B ) )  e. 
dom 
~~>  )
761, 2, 43, 47, 75isumrecl 13662 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  sum_ k  e.  NN  A  e.  RR )
7746simprd 461 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  0  <_  A )
781, 2, 43, 47, 75, 77isumge0 13663 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  0  <_ 
sum_ k  e.  NN  A )
79 elrege0 11630 . . . . . . 7  |-  ( sum_ k  e.  NN  A  e.  ( 0 [,) +oo ) 
<->  ( sum_ k  e.  NN  A  e.  RR  /\  0  <_ 
sum_ k  e.  NN  A ) )
8076, 78, 79sylanbrc 662 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  sum_ k  e.  NN  A  e.  ( 0 [,) +oo )
)
81 ssid 3508 . . . . . 6  |-  ( 0 [,) +oo )  C_  ( 0 [,) +oo )
8229, 33, 80, 81lmlimxrge0 28165 . . . . 5  |-  ( ( ( 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 ) )
8328, 82mpbird 232 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F
( ~~> t `  J
) sum_ k  e.  NN  A )
8416, 3syl5eqelr 2547 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  (
n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  e. 
dom 
~~>  )
8522eleq1d 2523 . . . . . . 7  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  ( (
n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  e. 
dom 
~~> 
<->  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A )  e.  dom  ~~>  ) )
8685adantr 463 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  e. 
dom 
~~> 
<->  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A )  e.  dom  ~~>  ) )
8784, 86mpbid 210 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  (
n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A )  e.  dom  ~~>  )
8844, 7, 87esumpcvgval 28307 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  -> Σ* k  e.  NN A  =  sum_ k  e.  NN  A )
8983, 88breqtrrd 4465 . . 3  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F
( ~~> t `  J
)Σ* k  e.  NN A
)
9032adantr 463 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F : NN --> ( 0 [,) +oo ) )
91 simpr 459 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  n  e.  NN )
9291nnzd 10964 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  n  e.  ZZ )
93 uzid 11096 . . . . . . . 8  |-  ( n  e.  ZZ  ->  n  e.  ( ZZ>= `  n )
)
94 peano2uz 11135 . . . . . . . 8  |-  ( n  e.  ( ZZ>= `  n
)  ->  ( n  +  1 )  e.  ( ZZ>= `  n )
)
9592, 93, 943syl 20 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( n  +  1 )  e.  ( ZZ>= `  n ) )
96 simplll 757 . . . . . . . 8  |-  ( ( ( ( ( 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 )
) )
9796, 13sylancom 665 . . . . . . 7  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  k  e.  NN )  ->  A  e.  ( 0 [,) +oo ) )
9891, 95, 97esumpmono 28308 . . . . . 6  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  <_ Σ* k  e.  ( 1 ... (
n  +  1 ) ) A )
9926, 21eqtr4d 2498 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  ( F `  n )  = Σ* k  e.  ( 1 ... n ) A )
10099adantlr 712 . . . . . 6  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( F `  n
)  = Σ* k  e.  ( 1 ... n ) A )
101 oveq2 6278 . . . . . . . . . . 11  |-  ( l  =  n  ->  (
1 ... l )  =  ( 1 ... n
) )
102 esumeq1 28263 . . . . . . . . . . 11  |-  ( ( 1 ... l )  =  ( 1 ... n )  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... n ) A )
103101, 102syl 16 . . . . . . . . . 10  |-  ( l  =  n  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... n ) A )
104103cbvmptv 4530 . . . . . . . . 9  |-  ( l  e.  NN  |-> Σ* k  e.  ( 1 ... l ) A )  =  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )
10516, 104eqtr4i 2486 . . . . . . . 8  |-  F  =  ( l  e.  NN  |-> Σ* k  e.  ( 1 ... l
) A )
106105a1i 11 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  F  =  ( l  e.  NN  |-> Σ* k  e.  ( 1 ... l ) A ) )
107 simpr3 1002 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  ( -.  F  e.  dom  ~~>  /\  n  e.  NN  /\  l  =  ( n  +  1 ) ) )  ->  l  =  ( n  +  1
) )
108 oveq2 6278 . . . . . . . . 9  |-  ( l  =  ( n  + 
1 )  ->  (
1 ... l )  =  ( 1 ... (
n  +  1 ) ) )
109 esumeq1 28263 . . . . . . . . 9  |-  ( ( 1 ... l )  =  ( 1 ... ( n  +  1 ) )  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... ( n  +  1 ) ) A )
110107, 108, 1093syl 20 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  ( -.  F  e.  dom  ~~>  /\  n  e.  NN  /\  l  =  ( n  +  1 ) ) )  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... ( n  +  1 ) ) A )
1111103anassrs 1216 . . . . . . 7  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  l  =  ( n  + 
1 ) )  -> Σ* k  e.  ( 1 ... l
) A  = Σ* k  e.  ( 1 ... (
n  +  1 ) ) A )
11291peano2nnd 10548 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( n  +  1 )  e.  NN )
113 ovex 6298 . . . . . . . 8  |-  ( 1 ... ( n  + 
1 ) )  e. 
_V
114 simp-4l 765 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  k  e.  ( 1 ... (
n  +  1 ) ) )  ->  ph )
115 elfznn 11717 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... ( n  +  1 ) )  ->  k  e.  NN )
116115adantl 464 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  k  e.  ( 1 ... (
n  +  1 ) ) )  ->  k  e.  NN )
117114, 116, 41syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  k  e.  ( 1 ... (
n  +  1 ) ) )  ->  A  e.  ( 0 [,] +oo ) )
118117ralrimiva 2868 . . . . . . . 8  |-  ( ( ( ( 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 ) )
119 nfcv 2616 . . . . . . . . 9  |-  F/_ k
( 1 ... (
n  +  1 ) )
120119esumcl 28259 . . . . . . . 8  |-  ( ( ( 1 ... (
n  +  1 ) )  e.  _V  /\  A. k  e.  ( 1 ... ( n  + 
1 ) ) A  e.  ( 0 [,] +oo ) )  -> Σ* k  e.  ( 1 ... ( n  +  1 ) ) A  e.  ( 0 [,] +oo ) )
121113, 118, 120sylancr 661 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... ( n  +  1 ) ) A  e.  ( 0 [,] +oo ) )
122106, 111, 112, 121fvmptd 5936 . . . . . 6  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( F `  (
n  +  1 ) )  = Σ* k  e.  ( 1 ... ( n  +  1 ) ) A )
12398, 100, 1223brtr4d 4469 . . . . 5  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( F `  n
)  <_  ( F `  ( n  +  1 ) ) )
124 simpr 459 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  -.  F  e.  dom  ~~>  )
12529, 90, 123, 124lmdvglim 28171 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F ( ~~> t `  J ) +oo )
126 nfv 1712 . . . . . . 7  |-  F/ k ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )
127 nfcv 2616 . . . . . . 7  |-  F/_ k NN
128 nnex 10537 . . . . . . . 8  |-  NN  e.  _V
129128a1i 11 . . . . . . 7  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  NN  e.  _V )
13041adantlr 712 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
131 simpr 459 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  x  e.  ( ~P NN  i^i  Fin ) )
132 simpll 751 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
) )
133 inss1 3704 . . . . . . . . . . . . . 14  |-  ( ~P NN  i^i  Fin )  C_ 
~P NN
134 simplr 753 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
135133, 134sseldi 3487 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  x  e.  ~P NN )
136135elpwid 4009 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  x  C_  NN )
137 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  k  e.  x )
138136, 137sseldd 3490 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  k  e.  NN )
139132, 138, 13syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  A  e.  ( 0 [,) +oo ) )
140 eqid 2454 . . . . . . . . . 10  |-  ( k  e.  x  |->  A )  =  ( k  e.  x  |->  A )
141139, 140fmptd 6031 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  (
k  e.  x  |->  A ) : x --> ( 0 [,) +oo ) )
142 esumpfinvallem 28303 . . . . . . . . 9  |-  ( ( x  e.  ( ~P NN  i^i  Fin )  /\  ( k  e.  x  |->  A ) : x --> ( 0 [,) +oo ) )  ->  (fld  gsumg  ( k  e.  x  |->  A ) )  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( k  e.  x  |->  A ) ) )
143131, 141, 142syl2anc 659 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  (fld  gsumg  ( k  e.  x  |->  A ) )  =  ( ( RR*ss  (
0 [,] +oo )
)  gsumg  ( k  e.  x  |->  A ) ) )
144 inss2 3705 . . . . . . . . . 10  |-  ( ~P NN  i^i  Fin )  C_ 
Fin
145144, 131sseldi 3487 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  x  e.  Fin )
146132, 138, 14syl2anc 659 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  /\  k  e.  x )  ->  A  e.  CC )
147145, 146gsumfsum 18679 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  (fld  gsumg  ( k  e.  x  |->  A ) )  = 
sum_ k  e.  x  A )
148143, 147eqtr3d 2497 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  (
( RR*ss  ( 0 [,] +oo ) )  gsumg  ( k  e.  x  |->  A ) )  = 
sum_ k  e.  x  A )
149126, 127, 129, 130, 148esumval 28275 . . . . . 6  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  -> Σ* k  e.  NN A  =  sup ( ran  ( x  e.  ( ~P NN  i^i  Fin )  |->  sum_ k  e.  x  A ) ,  RR* ,  <  ) )
150149adantr 463 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  -> Σ* k  e.  NN A  =  sup ( ran  ( x  e.  ( ~P NN  i^i  Fin )  |->  sum_ k  e.  x  A ) ,  RR* ,  <  ) )
15190, 123, 124lmdvg 28170 . . . . . . . . . . 11  |-  ( ( ( 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
) )
152151r19.21bi 2823 . . . . . . . . . 10  |-  ( ( ( ( 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
) )
153 nnz 10882 . . . . . . . . . . . . 13  |-  ( l  e.  NN  ->  l  e.  ZZ )
154 uzid 11096 . . . . . . . . . . . . 13  |-  ( l  e.  ZZ  ->  l  e.  ( ZZ>= `  l )
)
155153, 154syl 16 . . . . . . . . . . . 12  |-  ( l  e.  NN  ->  l  e.  ( ZZ>= `  l )
)
156 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( l  e.  NN  /\  n  =  l )  ->  n  =  l )
157156fveq2d 5852 . . . . . . . . . . . . 13  |-  ( ( l  e.  NN  /\  n  =  l )  ->  ( F `  n
)  =  ( F `
 l ) )
158157breq2d 4451 . . . . . . . . . . . 12  |-  ( ( l  e.  NN  /\  n  =  l )  ->  ( y  <  ( F `  n )  <->  y  <  ( F `  l ) ) )
159155, 158rspcdv 3210 . . . . . . . . . . 11  |-  ( l  e.  NN  ->  ( A. n  e.  ( ZZ>=
`  l ) y  <  ( F `  n )  ->  y  <  ( F `  l
) ) )
160159reximia 2920 . . . . . . . . . 10  |-  ( E. l  e.  NN  A. n  e.  ( ZZ>= `  l ) y  < 
( F `  n
)  ->  E. l  e.  NN  y  <  ( F `  l )
)
161152, 160syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  y  e.  RR )  ->  E. l  e.  NN  y  <  ( F `  l ) )
162 simplr 753 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  y  e.  RR )
16390ad2antrr 723 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  F : NN --> ( 0 [,) +oo ) )
164 simpr 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  l  e.  NN )
165163, 164ffvelrnd 6008 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  ( F `  l )  e.  ( 0 [,) +oo ) )
1664, 165sseldi 3487 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  ( F `  l )  e.  RR )
167 ltle 9662 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  ( F `  l )  e.  RR )  -> 
( y  <  ( F `  l )  ->  y  <_  ( F `  l ) ) )
168162, 166, 167syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  (
y  <  ( F `  l )  ->  y  <_  ( F `  l
) ) )
16916a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  F  =  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A ) )
170 oveq2 6278 . . . . . . . . . . . . . . . 16  |-  ( n  =  l  ->  (
1 ... n )  =  ( 1 ... l
) )
171 esumeq1 28263 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... n )  =  ( 1 ... l )  -> Σ* k  e.  ( 1 ... n ) A  = Σ* k  e.  ( 1 ... l ) A )
172170, 171syl 16 . . . . . . . . . . . . . . 15  |-  ( n  =  l  -> Σ* k  e.  ( 1 ... n ) A  = Σ* k  e.  ( 1 ... l ) A )
173172adantl 464 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  /\  -.  F  e.  dom  ~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  /\  n  =  l )  -> Σ* k  e.  ( 1 ... n
) A  = Σ* k  e.  ( 1 ... l
) A )
174 esumex 28258 . . . . . . . . . . . . . . 15  |- Σ* k  e.  ( 1 ... l ) A  e.  _V
175174a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  -> Σ* k  e.  ( 1 ... l ) A  e.  _V )
176169, 173, 164, 175fvmptd 5936 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  ( F `  l )  = Σ* k  e.  ( 1 ... l ) A )
177 fzfid 12065 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  (
1 ... l )  e. 
Fin )
178 simp-4l 765 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
) )
179 elfznn 11717 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... l )  ->  k  e.  NN )
180179adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
181178, 180, 13syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 ) )
182177, 181esumpfinval 28304 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  -> Σ* k  e.  ( 1 ... l ) A  =  sum_ k  e.  ( 1 ... l
) A )
183176, 182eqtrd 2495 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 )
184183breq2d 4451 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
185168, 184sylibd 214 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
186185reximdva 2929 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
187161, 186mpd 15 . . . . . . . 8  |-  ( ( ( ( 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 )
188 fzssuz 11728 . . . . . . . . . . . . . 14  |-  ( 1 ... l )  C_  ( ZZ>= `  1 )
189188, 1sseqtr4i 3522 . . . . . . . . . . . . 13  |-  ( 1 ... l )  C_  NN
190 ovex 6298 . . . . . . . . . . . . . 14  |-  ( 1 ... l )  e. 
_V
191190elpw 4005 . . . . . . . . . . . . 13  |-  ( ( 1 ... l )  e.  ~P NN  <->  ( 1 ... l )  C_  NN )
192189, 191mpbir 209 . . . . . . . . . . . 12  |-  ( 1 ... l )  e. 
~P NN
193 fzfi 12064 . . . . . . . . . . . 12  |-  ( 1 ... l )  e. 
Fin
194 elin 3673 . . . . . . . . . . . 12  |-  ( ( 1 ... l )  e.  ( ~P NN  i^i  Fin )  <->  ( (
1 ... l )  e. 
~P NN  /\  (
1 ... l )  e. 
Fin ) )
195192, 193, 194mpbir2an 918 . . . . . . . . . . 11  |-  ( 1 ... l )  e.  ( ~P NN  i^i  Fin )
196 sumex 13592 . . . . . . . . . . 11  |-  sum_ k  e.  ( 1 ... l
) A  e.  _V
197 eqid 2454 . . . . . . . . . . . 12  |-  ( x  e.  ( ~P NN  i^i  Fin )  |->  sum_ k  e.  x  A )  =  ( x  e.  ( ~P NN  i^i  Fin )  |->  sum_ k  e.  x  A )
198 sumeq1 13593 . . . . . . . . . . . 12  |-  ( x  =  ( 1 ... l )  ->  sum_ k  e.  x  A  =  sum_ k  e.  ( 1 ... l ) A )
199197, 198elrnmpt1s 5239 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
200195, 196, 199mp2an 670 . . . . . . . . . 10  |-  sum_ k  e.  ( 1 ... l
) A  e.  ran  ( x  e.  ( ~P NN  i^i  Fin )  |-> 
sum_ k  e.  x  A )
201 nfv 1712 . . . . . . . . . . 11  |-  F/ z  y  <_  sum_ k  e.  ( 1 ... l
) A
202 breq2 4443 . . . . . . . . . . 11  |-  ( z  =  sum_ k  e.  ( 1 ... l ) A  ->  ( y  <_  z  <->  y  <_  sum_ k  e.  ( 1 ... l
) A ) )
203201, 202rspce 3202 . . . . . . . . . 10  |-  ( (
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 )
204200, 203mpan 668 . . . . . . . . 9  |-  ( 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 )
205204rexlimivw 2943 . . . . . . . 8  |-  ( 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 )
206187, 205syl 16 . . . . . . 7  |-  ( ( ( ( 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 )
207206ralrimiva 2868 . . . . . 6  |-  ( ( ( 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 )
208 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
209144, 208sseldi 3487 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  x  e.  Fin )
210139adantllr 716 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) )
2114, 210sseldi 3487 . . . . . . . . . 10  |-  ( ( ( ( ( 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 )
212209, 211fsumrecl 13638 . . . . . . . . 9  |-  ( ( ( ( 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 )
213212rexrd 9632 . . . . . . . 8  |-  ( ( ( ( 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* )
214213, 197fmptd 6031 . . . . . . 7  |-  ( ( ( 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* )
215 frn 5719 . . . . . . 7  |-  ( ( 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* )
216 supxrunb1 11514 . . . . . . 7  |-  ( 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 ) )
217214, 215, 2163syl 20 . . . . . 6  |-  ( ( ( 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 ) )
218207, 217mpbid 210 . . . . 5  |-  ( ( ( 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 )
219150, 218eqtrd 2495 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  -> Σ* k  e.  NN A  = +oo )
220125, 219breqtrrd 4465 . . 3  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
22189, 220pm2.61dan 789 . 2  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F ( ~~> t `  J )Σ* k  e.  NN A )
22216reseq1i 5258 . . . . . . . 8  |-  ( F  |`  ( ZZ>= `  k )
)  =  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
)
223 eleq1 2526 . . . . . . . . . . . 12  |-  ( l  =  k  ->  (
l  e.  NN  <->  k  e.  NN ) )
224223anbi2d 701 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( ph  /\  l  e.  NN )  <->  ( ph  /\  k  e.  NN ) ) )
225 sbequ12r 1998 . . . . . . . . . . 11  |-  ( l  =  k  ->  ( [ l  /  k ] A  = +oo  <->  A  = +oo ) )
226224, 225anbi12d 708 . . . . . . . . . 10  |-  ( l  =  k  ->  (
( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo ) 
<->  ( ( ph  /\  k  e.  NN )  /\  A  = +oo ) ) )
227 fveq2 5848 . . . . . . . . . . . 12  |-  ( l  =  k  ->  ( ZZ>=
`  l )  =  ( ZZ>= `  k )
)
228227reseq2d 5262 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  l )
)  =  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
) )
229227xpeq1d 5011 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( ZZ>= `  l )  X.  { +oo } )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )
230228, 229eqeq12d 2476 . . . . . . . . . 10  |-  ( l  =  k  ->  (
( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>= `  l ) )  =  ( ( ZZ>= `  l
)  X.  { +oo } )  <->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>=
`  k ) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) ) )
231226, 230imbi12d 318 . . . . . . . . 9  |-  ( l  =  k  ->  (
( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  l )
)  =  ( (
ZZ>= `  l )  X. 
{ +oo } ) )  <-> 
( ( ( ph  /\  k  e.  NN )  /\  A  = +oo )  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>=
`  k ) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) ) ) )
232 nfv 1712 . . . . . . . . . . . . . 14  |-  F/ k ( ph  /\  l  e.  NN )
233 nfs1v 2183 . . . . . . . . . . . . . 14  |-  F/ k [ l  /  k ] A  = +oo
234232, 233nfan 1933 . . . . . . . . . . . . 13  |-  F/ k ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )
235 nfv 1712 . . . . . . . . . . . . 13  |-  F/ k  n  e.  ( ZZ>= `  l )
236234, 235nfan 1933 . . . . . . . . . . . 12  |-  F/ k ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)
23748a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  ( 1 ... n )  e.  _V )
238 simp-4l 765 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  ph )
23918adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
240238, 239, 41syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,] +oo ) )
241 simpllr 758 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  l  e.  NN )
242 elnnuz 11118 . . . . . . . . . . . . . . 15  |-  ( l  e.  NN  <->  l  e.  ( ZZ>= `  1 )
)
243 eluzfz 11686 . . . . . . . . . . . . . . 15  |-  ( ( l  e.  ( ZZ>= ` 
1 )  /\  n  e.  ( ZZ>= `  l )
)  ->  l  e.  ( 1 ... n
) )
244242, 243sylanb 470 . . . . . . . . . . . . . 14  |-  ( ( l  e.  NN  /\  n  e.  ( ZZ>= `  l ) )  -> 
l  e.  ( 1 ... n ) )
245241, 244sylancom 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  l  e.  ( 1 ... n ) )
246 simplr 753 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  [ l  / 
k ] A  = +oo )
247 sbequ12 1997 . . . . . . . . . . . . . 14  |-  ( k  =  l  ->  ( A  = +oo  <->  [ l  /  k ] A  = +oo ) )
248233, 247rspce 3202 . . . . . . . . . . . . 13  |-  ( ( l  e.  ( 1 ... n )  /\  [ l  /  k ] A  = +oo )  ->  E. k  e.  ( 1 ... n ) A  = +oo )
249245, 246, 248syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  E. k  e.  ( 1 ... n ) A  = +oo )
250236, 237, 240, 249esumpinfval 28302 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  -> Σ* k  e.  ( 1 ... n ) A  = +oo )
251250ralrimiva 2868 . . . . . . . . . 10  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  A. n  e.  (
ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )
252 eqidd 2455 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  ( ZZ>= `  l )  =  ( ZZ>= `  l
) )
253 mpteq12 4518 . . . . . . . . . . . 12  |-  ( ( ( ZZ>= `  l )  =  ( ZZ>= `  l
)  /\  A. n  e.  ( ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )  ->  ( n  e.  ( ZZ>= `  l )  |-> Σ* k  e.  ( 1 ... n ) A )  =  ( n  e.  ( ZZ>= `  l )  |-> +oo ) )
254252, 253sylan 469 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  A. n  e.  ( ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )  ->  ( n  e.  ( ZZ>= `  l )  |-> Σ* k  e.  ( 1 ... n ) A )  =  ( n  e.  ( ZZ>= `  l )  |-> +oo ) )
255 simplr 753 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  l  e.  NN )
256 uznnssnn 11129 . . . . . . . . . . . . 13  |-  ( l  e.  NN  ->  ( ZZ>=
`  l )  C_  NN )
257 resmpt 5311 . . . . . . . . . . . . 13  |-  ( (
ZZ>= `  l )  C_  NN  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>=
`  l ) )  =  ( n  e.  ( ZZ>= `  l )  |-> Σ* k  e.  ( 1 ... n ) A ) )
258255, 256, 2573syl 20 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>= `  l ) )  =  ( n  e.  (
ZZ>= `  l )  |-> Σ* k  e.  ( 1 ... n
) A ) )
259258adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  A. n  e.  ( ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>=
`  l ) )  =  ( n  e.  ( ZZ>= `  l )  |-> Σ* k  e.  ( 1 ... n ) A ) )
260 fconstmpt 5032 . . . . . . . . . . . 12  |-  ( (
ZZ>= `  l )  X. 
{ +oo } )  =  ( n  e.  (
ZZ>= `  l )  |-> +oo )
261260a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  A. n  e.  ( ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )  ->  ( ( ZZ>= `  l )  X.  { +oo } )  =  ( n  e.  ( ZZ>= `  l )  |-> +oo )
)
262254, 259, 2613eqtr4d 2505 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  A. n  e.  ( ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>=
`  l ) )  =  ( ( ZZ>= `  l )  X.  { +oo } ) )
263251, 262mpdan 666 . . . . . . . . 9  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n ) A )  |`  ( ZZ>= `  l ) )  =  ( ( ZZ>= `  l
)  X.  { +oo } ) )
264231, 263chvarv 2019 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  A  = +oo )  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
)  =  ( (
ZZ>= `  k )  X. 
{ +oo } ) )
265222, 264syl5eq 2507 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  A  = +oo )  ->  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )
266265ex 432 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( A  = +oo  ->  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) ) )
267266reximdva 2929 . . . . 5  |-  ( ph  ->  ( E. k  e.  NN  A  = +oo  ->  E. k  e.  NN  ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } ) ) )
268267imp 427 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  E. k  e.  NN  ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } ) )
269 xrge0topn 28160 . . . . . . . . . . 11  |-  ( TopOpen `  ( RR*ss  ( 0 [,] +oo ) ) )  =  ( (ordTop `  <_  )t  ( 0 [,] +oo )
)
27029, 269eqtri 2483 . . . . . . . . . 10  |-  J  =  ( (ordTop `  <_  )t  ( 0 [,] +oo )
)
271 letopon 19873 . . . . . . . . . . 11  |-  (ordTop `  <_  )  e.  (TopOn `  RR* )
272 iccssxr 11610 . . . . . . . . . . 11  |-  ( 0 [,] +oo )  C_  RR*
273 resttopon 19829 . . . . . . . . . . 11  |-  ( ( (ordTop `  <_  )  e.  (TopOn `  RR* )  /\  ( 0 [,] +oo )  C_  RR* )  ->  (
(ordTop `  <_  )t  ( 0 [,] +oo ) )  e.  (TopOn `  (
0 [,] +oo )
) )
274271, 272, 273mp2an 670 . . . . . . . . . 10  |-  ( (ordTop `  <_  )t  ( 0 [,] +oo ) )  e.  (TopOn `  ( 0 [,] +oo ) )
275270, 274eqeltri 2538 . . . . . . . . 9  |-  J  e.  (TopOn `  ( 0 [,] +oo ) )
276275a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  J  e.  (TopOn `  ( 0 [,] +oo ) ) )
277 0xr 9629 . . . . . . . . . 10  |-  0  e.  RR*
278 pnfxr 11324 . . . . . . . . . 10  |- +oo  e.  RR*
279 0lepnf 11343 . . . . . . . . . 10  |-  0  <_ +oo
280 ubicc2 11640 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  -> +oo  e.  ( 0 [,] +oo ) )
281277, 278, 279, 280mp3an 1322 . . . . . . . . 9  |- +oo  e.  ( 0 [,] +oo )
282281a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  -> +oo  e.  ( 0 [,] +oo ) )
28340nnzd 10964 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
284 eqid 2454 . . . . . . . . 9  |-  ( ZZ>= `  k )  =  (
ZZ>= `  k )
285284lmconst 19929 . . . . . . . 8  |-  ( ( J  e.  (TopOn `  ( 0 [,] +oo ) )  /\ +oo  e.  ( 0 [,] +oo )  /\  k  e.  ZZ )  ->  ( ( ZZ>= `  k )  X.  { +oo } ) ( ~~> t `  J ) +oo )
286276, 282, 283, 285syl3anc 1226 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ZZ>= `  k )  X. 
{ +oo } ) ( ~~> t `  J ) +oo )
287 breq1 4442 . . . . . . . 8  |-  ( ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } )  ->  ( ( F  |`  ( ZZ>= `  k
) ) ( ~~> t `  J ) +oo  <->  ( ( ZZ>=
`  k )  X. 
{ +oo } ) ( ~~> t `  J ) +oo ) )
288287biimprd 223 . . . . . . 7  |-  ( ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } )  ->  ( (
( ZZ>= `  k )  X.  { +oo } ) ( ~~> t `  J
) +oo  ->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
)
289286, 288mpan9 467 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )  ->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
290276elfvexd 5876 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 0 [,] +oo )  e. 
_V )
291 cnex 9562 . . . . . . . . . 10  |-  CC  e.  _V
292291a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  CC  e.  _V )
29356adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  F : NN
--> ( 0 [,] +oo ) )
294 nnsscn 10536 . . . . . . . . . 10  |-  NN  C_  CC
295294a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  NN  C_  CC )
296 elpm2r 7429 . . . . . . . . 9  |-  ( ( ( ( 0 [,] +oo )  e.  _V  /\  CC  e.  _V )  /\  ( F : NN --> ( 0 [,] +oo )  /\  NN  C_  CC ) )  ->  F  e.  ( ( 0 [,] +oo )  ^pm  CC ) )
297290, 292, 293, 295, 296syl22anc 1227 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  F  e.  ( ( 0 [,] +oo )  ^pm  CC ) )
298276, 297, 283lmres 19968 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( F ( ~~> t `  J
) +oo  <->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
)
299298biimpar 483 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) ) ( ~~> t `  J ) +oo )  ->  F ( ~~> t `  J ) +oo )
300289, 299syldan 468 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )  ->  F ( ~~> t `  J ) +oo )
301300r19.29an 2995 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  ( F  |`  ( ZZ>= `  k )
)  =  ( (
ZZ>= `  k )  X. 
{ +oo } ) )  ->  F ( ~~> t `  J ) +oo )
302268, 301syldan 468 . . 3  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  F ( ~~> t `  J ) +oo )
303 nfv 1712 . . . . 5  |-  F/ k
ph
304 nfre1 2915 . . . . 5  |-  F/ k E. k  e.  NN  A  = +oo
305303, 304nfan 1933 . . . 4  |-  F/ k ( ph  /\  E. k  e.  NN  A  = +oo )
306128a1i 11 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  NN  e.  _V )
30741adantlr 712 . . . 4  |-  ( ( ( ph  /\  E. k  e.  NN  A  = +oo )  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
308 simpr 459 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  E. k  e.  NN  A  = +oo )
309305, 306, 307, 308esumpinfval 28302 . . 3  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  -> Σ* k  e.  NN A  = +oo )
310302, 309breqtrrd 4465 . 2  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
311 eleq1 2526 . . . . . . . . 9  |-  ( k  =  m  ->  (
k  e.  NN  <->  m  e.  NN ) )
312311anbi2d 701 . . . . . . . 8  |-  ( k  =  m  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  m  e.  NN ) ) )
3137eleq1d 2523 . . . . . . . 8  |-  ( k  =  m  ->  ( A  e.  ( 0 [,] +oo )  <->  B  e.  ( 0 [,] +oo ) ) )
314312, 313imbi12d 318 . . . . . . 7  |-  ( k  =  m  ->  (
( ( ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )  <-> 
( ( ph  /\  m  e.  NN )  ->  B  e.  ( 0 [,] +oo ) ) ) )
315314, 41chvarv 2019 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  B  e.  ( 0 [,] +oo ) )
316 eliccelico 27822 . . . . . . 7  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  ->  ( B  e.  ( 0 [,] +oo )  <->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) ) )
317277, 278, 279, 316mp3an 1322 . . . . . 6  |-  ( B  e.  ( 0 [,] +oo )  <->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) )
318315, 317sylib 196 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) )
319318ralrimiva 2868 . . . 4  |-  ( ph  ->  A. m  e.  NN  ( B  e.  (
0 [,) +oo )  \/  B  = +oo ) )
320 r19.30 2999 . . . 4  |-  ( A. m  e.  NN  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo )  ->  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  \/  E. m  e.  NN  B  = +oo )
)
321319, 320syl 16 . . 3  |-  ( ph  ->  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  \/  E. m  e.  NN  B  = +oo )
)
3227eqeq1d 2456 . . . . 5  |-  ( k  =  m  ->  ( A  = +oo  <->  B  = +oo ) )
323322cbvrexv 3082 . . . 4  |-  ( E. k  e.  NN  A  = +oo  <->  E. m  e.  NN  B  = +oo )
324323orbi2i 517 . . 3  |-  ( ( 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 )
)
325321, 324sylibr 212 . 2  |-  ( ph  ->  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  \/  E. k  e.  NN  A  = +oo )
)
326221, 310, 325mpjaodan 784 1  |-  ( ph  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398   [wsb 1744    e. wcel 1823   A.wral 2804   E.wrex 2805   _Vcvv 3106    i^i cin 3460    C_ wss 3461   ~Pcpw 3999   {csn 4016   class class class wbr 4439    |-> cmpt 4497    X. cxp 4986   dom cdm 4988   ran crn 4989    |` cres 4990    Fn wfn 5565   -->wf 5566   ` cfv 5570  (class class class)co 6270    ^pm cpm 7413   Fincfn 7509   supcsup 7892   CCcc 9479   RRcr 9480   0cc0 9481   1c1 9482    + caddc 9484   +oocpnf 9614   RR*cxr 9616    < clt 9617    <_ cle 9618   NNcn 10531   ZZcz 10860   ZZ>=cuz 11082   [,)cico 11534   [,]cicc 11535   ...cfz 11675    seqcseq 12089    ~~> cli 13389   sum_csu 13590   ↾s cress 14717   ↾t crest 14910   TopOpenctopn 14911    gsumg cgsu 14930  ordTopcordt 14988   RR*scxrs 14989  ℂfldccnfld 18615  TopOnctopon 19562   ~~> tclm 19894  Σ*cesum 28256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559  ax-addf 9560  ax-mulf 9561
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-iin 4318  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-of 6513  df-om 6674  df-1st 6773  df-2nd 6774  df-supp 6892  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7463  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fsupp 7822  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ioc 11537  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-fl 11910  df-mod 11979  df-seq 12090  df-exp 12149  df-fac 12336  df-bc 12363  df-hash 12388  df-shft 12982  df-cj 13014  df-re 13015  df-im 13016  df-sqrt 13150  df-abs 13151  df-limsup 13376  df-clim 13393  df-rlim 13394  df-sum 13591  df-ef 13885  df-sin 13887  df-cos 13888  df-pi 13890  df-struct 14718  df-ndx 14719  df-slot 14720  df-base 14721  df-sets 14722  df-ress 14723  df-plusg 14797  df-mulr 14798  df-starv 14799  df-sca 14800  df-vsca 14801  df-ip 14802  df-tset 14803  df-ple 14804  df-ds 14806  df-unif 14807  df-hom 14808  df-cco 14809  df-rest 14912  df-topn 14913  df-0g 14931  df-gsum 14932  df-topgen 14933  df-pt 14934  df-prds 14937  df-ordt 14990  df-xrs 14991  df-qtop 14996  df-imas 14997  df-xps 14999  df-mre 15075  df-mrc 15076  df-acs 15078  df-ps 16029  df-tsr 16030  df-plusf 16070  df-mgm 16071  df-sgrp 16110  df-mnd 16120  df-mhm 16165  df-submnd 16166  df-grp 16256  df-minusg 16257  df-sbg 16258  df-mulg 16259  df-subg 16397  df-cntz 16554  df-cmn 16999  df-abl 17000  df-mgp 17337  df-ur 17349  df-ring 17395  df-cring 17396  df-subrg 17622  df-abv 17661  df-lmod 17709  df-scaf 17710  df-sra 18013  df-rgmod 18014  df-psmet 18606  df-xmet 18607  df-met 18608  df-bl 18609  df-mopn 18610  df-fbas 18611  df-fg 18612  df-cnfld 18616  df-top 19566  df-bases 19568  df-topon 19569  df-topsp 19570  df-cld 19687  df-ntr 19688  df-cls 19689  df-nei 19766  df-lp 19804  df-perf 19805  df-cn 19895  df-cnp 19896  df-lm 19897  df-haus 19983  df-tx 20229  df-hmeo 20422  df-fil 20513  df-fm 20605  df-flim 20606  df-flf 20607  df-tmd 20737  df-tgp 20738  df-tsms 20791  df-trg 20828  df-xms 20989  df-ms 20990  df-tms 20991  df-nm 21269  df-ngp 21270  df-nrg 21272  df-nlm 21273  df-ii 21547  df-cncf 21548  df-limc 22436  df-dv 22437  df-log 23110  df-esum 28257
This theorem is referenced by:  esumcvg2  28316
  Copyright terms: Public domain W3C validator