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

Theorem esumcvg 28956
Description: The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 13842. (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 11223 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
2 1zzd 10997 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  1  e.  ZZ )
3 simpr 467 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F  e.  dom  ~~>  )
4 rge0ssre 11769 . . . . . . . . 9  |-  ( 0 [,) +oo )  C_  RR
5 ax-resscn 9622 . . . . . . . . 9  |-  RR  C_  CC
64, 5sstri 3453 . . . . . . . 8  |-  ( 0 [,) +oo )  C_  CC
7 esumcvg.m . . . . . . . . . . . . 13  |-  ( k  =  m  ->  A  =  B )
87eleq1d 2524 . . . . . . . . . . . 12  |-  ( k  =  m  ->  ( A  e.  ( 0 [,) +oo )  <->  B  e.  ( 0 [,) +oo ) ) )
98cbvralv 3031 . . . . . . . . . . 11  |-  ( A. k  e.  NN  A  e.  ( 0 [,) +oo ) 
<-> 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )
10 rsp 2766 . . . . . . . . . . 11  |-  ( A. k  e.  NN  A  e.  ( 0 [,) +oo )  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
119, 10sylbir 218 . . . . . . . . . 10  |-  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
1211adantl 472 . . . . . . . . 9  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  ( k  e.  NN  ->  A  e.  ( 0 [,) +oo ) ) )
1312imp 435 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  ( 0 [,) +oo ) )
146, 13sseldi 3442 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  CC )
1514adantlr 726 . . . . . 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 12218 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  (
1 ... n )  e. 
Fin )
18 elfznn 11857 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... n )  ->  k  e.  NN )
1918, 13sylan2 481 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,) +oo ) )
2019adantlr 726 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,) +oo ) )
2117, 20esumpfinval 28945 . . . . . . . . . 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 4503 . . . . . . . . 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 2508 . . . . . . . 8  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  =  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A ) )
246, 20sseldi 3442 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  CC )
2517, 24fsumcl 13848 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) A  e.  CC )
2623, 25fvmpt2d 5982 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  ( F `  n )  =  sum_ k  e.  ( 1 ... n ) A )
2726adantlr 726 . . . . . 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 13869 . . . . 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 28507 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  sum_ k  e.  ( 1 ... n
) A  e.  ( 0 [,) +oo )
)
3121, 30eqeltrd 2540 . . . . . . . 8  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  e.  ( 0 [,) +oo ) )
3231, 16fmptd 6069 . . . . . . 7  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F : NN
--> ( 0 [,) +oo ) )
3332adantr 471 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F : NN --> ( 0 [,) +oo ) )
34 simplll 773 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  ph )
35 eqidd 2463 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( m  e.  NN  |->  B )  =  ( m  e.  NN  |->  B ) )
36 eqcom 2469 . . . . . . . . . . . 12  |-  ( k  =  m  <->  m  =  k )
37 eqcom 2469 . . . . . . . . . . . 12  |-  ( A  =  B  <->  B  =  A )
387, 36, 373imtr3i 273 . . . . . . . . . . 11  |-  ( m  =  k  ->  B  =  A )
3938adantl 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  =  k )  ->  B  =  A )
40 simpr 467 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
41 esumcvg.a . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
4235, 39, 40, 41fvmptd 5977 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( m  e.  NN  |->  B ) `  k )  =  A )
4334, 42sylancom 678 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  (
( m  e.  NN  |->  B ) `  k
)  =  A )
4413adantlr 726 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  A  e.  ( 0 [,) +oo ) )
45 elrege0 11767 . . . . . . . . . 10  |-  ( A  e.  ( 0 [,) +oo )  <->  ( A  e.  RR  /\  0  <_  A ) )
4644, 45sylib 201 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  ( A  e.  RR  /\  0  <_  A ) )
4746simpld 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  A  e.  RR )
48 ovex 6343 . . . . . . . . . . . . . . 15  |-  ( 1 ... n )  e. 
_V
49 simpll 765 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ph )
5018adantl 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
5149, 50, 41syl2anc 671 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,] +oo ) )
5251ralrimiva 2814 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  A. k  e.  ( 1 ... n
) A  e.  ( 0 [,] +oo )
)
53 nfcv 2603 . . . . . . . . . . . . . . . 16  |-  F/_ k
( 1 ... n
)
5453esumcl 28900 . . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  -> Σ* k  e.  ( 1 ... n ) A  e.  ( 0 [,] +oo ) )
5655, 16fmptd 6069 . . . . . . . . . . . . 13  |-  ( ph  ->  F : NN --> ( 0 [,] +oo ) )
57 ffn 5751 . . . . . . . . . . . . 13  |-  ( F : NN --> ( 0 [,] +oo )  ->  F  Fn  NN )
5856, 57syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  F  Fn  NN )
5958adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  Fn  NN )
60 1z 10996 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
61 seqfn 12257 . . . . . . . . . . . . . 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 5693 . . . . . . . . . . . . 13  |-  (  seq 1 (  +  , 
( m  e.  NN  |->  B ) )  Fn  NN  <->  seq 1 (  +  ,  ( m  e.  NN  |->  B ) )  Fn  ( ZZ>= `  1
) )
6462, 63mpbir 214 . . . . . . . . . . . 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 773 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  /\  k  e.  ( 1 ... n
) )  ->  ph )
6718, 42sylan2 481 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 1 ... n
) )  ->  (
( m  e.  NN  |->  B ) `  k
)  =  A )
6866, 67sylancom 678 . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  n  e.  NN )
7069, 1syl6eleq 2550 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
7168, 70, 24fsumser 13845 . . . . . . . . . . . 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 2496 . . . . . . . . . . 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 6002 . . . . . . . . . 10  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F  =  seq 1 (  +  , 
( m  e.  NN  |->  B ) ) )
7473adantr 471 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F  =  seq 1 (  +  ,  ( m  e.  NN  |->  B ) ) )
7574, 3eqeltrrd 2541 . . . . . . . 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 13875 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  sum_ k  e.  NN  A  e.  RR )
7746simprd 469 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  /\  k  e.  NN )  ->  0  <_  A )
781, 2, 43, 47, 75, 77isumge0 13876 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  0  <_ 
sum_ k  e.  NN  A )
79 elrege0 11767 . . . . . . 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 675 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  sum_ k  e.  NN  A  e.  ( 0 [,) +oo )
)
81 ssid 3463 . . . . . 6  |-  ( 0 [,) +oo )  C_  ( 0 [,) +oo )
8229, 33, 80, 81lmlimxrge0 28803 . . . . 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 240 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F
( ~~> t `  J
) sum_ k  e.  NN  A )
8416, 3syl5eqelr 2545 . . . . . 6  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  (
n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  e. 
dom 
~~>  )
8522eleq1d 2524 . . . . . . 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 471 . . . . . 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 215 . . . . 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 28948 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  -> Σ* k  e.  NN A  =  sum_ k  e.  NN  A )
8983, 88breqtrrd 4443 . . 3  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  F  e.  dom  ~~>  )  ->  F
( ~~> t `  J
)Σ* k  e.  NN A
)
9032adantr 471 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F : NN --> ( 0 [,) +oo ) )
91 simpr 467 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  n  e.  NN )
9291nnzd 11068 . . . . . . . 8  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  n  e.  ZZ )
93 uzid 11202 . . . . . . . 8  |-  ( n  e.  ZZ  ->  n  e.  ( ZZ>= `  n )
)
94 peano2uz 11241 . . . . . . . 8  |-  ( n  e.  ( ZZ>= `  n
)  ->  ( n  +  1 )  e.  ( ZZ>= `  n )
)
9592, 93, 943syl 18 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( n  +  1 )  e.  ( ZZ>= `  n ) )
96 simplll 773 . . . . . . . 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 678 . . . . . . 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 28949 . . . . . 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 2499 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  n  e.  NN )  ->  ( F `  n )  = Σ* k  e.  ( 1 ... n ) A )
10099adantlr 726 . . . . . 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 6323 . . . . . . . . . . 11  |-  ( l  =  n  ->  (
1 ... l )  =  ( 1 ... n
) )
102 esumeq1 28904 . . . . . . . . . . 11  |-  ( ( 1 ... l )  =  ( 1 ... n )  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... n ) A )
103101, 102syl 17 . . . . . . . . . 10  |-  ( l  =  n  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... n ) A )
104103cbvmptv 4509 . . . . . . . . 9  |-  ( l  e.  NN  |-> Σ* k  e.  ( 1 ... l ) A )  =  ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )
10516, 104eqtr4i 2487 . . . . . . . 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 1022 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  ( -.  F  e.  dom  ~~>  /\  n  e.  NN  /\  l  =  ( n  +  1 ) ) )  ->  l  =  ( n  +  1
) )
108 oveq2 6323 . . . . . . . . 9  |-  ( l  =  ( n  + 
1 )  ->  (
1 ... l )  =  ( 1 ... (
n  +  1 ) ) )
109 esumeq1 28904 . . . . . . . . 9  |-  ( ( 1 ... l )  =  ( 1 ... ( n  +  1 ) )  -> Σ* k  e.  ( 1 ... l ) A  = Σ* k  e.  ( 1 ... ( n  +  1 ) ) A )
110107, 108, 1093syl 18 . . . . . . . 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 1240 . . . . . . 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 10654 . . . . . . 7  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( n  +  1 )  e.  NN )
113 ovex 6343 . . . . . . . 8  |-  ( 1 ... ( n  + 
1 ) )  e. 
_V
114 simp-4l 781 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  n  e.  NN )  /\  k  e.  ( 1 ... (
n  +  1 ) ) )  ->  ph )
115 elfznn 11857 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... ( n  +  1 ) )  ->  k  e.  NN )
116115adantl 472 . . . . . . . . . 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 671 . . . . . . . . 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 2814 . . . . . . . 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 2603 . . . . . . . . 9  |-  F/_ k
( 1 ... (
n  +  1 ) )
120119esumcl 28900 . . . . . . . 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 674 . . . . . . 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 5977 . . . . . 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 4447 . . . . 5  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  n  e.  NN )  ->  ( F `  n
)  <_  ( F `  ( n  +  1 ) ) )
124 simpr 467 . . . . 5  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  -.  F  e.  dom  ~~>  )
12529, 90, 123, 124lmdvglim 28809 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F ( ~~> t `  J ) +oo )
126 nfv 1772 . . . . . . 7  |-  F/ k ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )
127 nfcv 2603 . . . . . . 7  |-  F/_ k NN
128 nnex 10643 . . . . . . . 8  |-  NN  e.  _V
129128a1i 11 . . . . . . 7  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  NN  e.  _V )
13041adantlr 726 . . . . . . 7  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
131 simpr 467 . . . . . . . . 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 765 . . . . . . . . . . 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 3664 . . . . . . . . . . . . . 14  |-  ( ~P NN  i^i  Fin )  C_ 
~P NN
134 simplr 767 . . . . . . . . . . . . . 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 3442 . . . . . . . . . . . . 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 3973 . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 3445 . . . . . . . . . . 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 671 . . . . . . . . . 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 2462 . . . . . . . . . 10  |-  ( k  e.  x  |->  A )  =  ( k  e.  x  |->  A )
141139, 140fmptd 6069 . . . . . . . . 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 28944 . . . . . . . . 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 671 . . . . . . . 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 3665 . . . . . . . . . 10  |-  ( ~P NN  i^i  Fin )  C_ 
Fin
145144, 131sseldi 3442 . . . . . . . . 9  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  x  e.  Fin )
146132, 138, 14syl2anc 671 . . . . . . . . 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 19083 . . . . . . . 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 2498 . . . . . . 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 28916 . . . . . 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 471 . . . . 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 28808 . . . . . . . . . . 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 2769 . . . . . . . . . 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 10988 . . . . . . . . . . . . 13  |-  ( l  e.  NN  ->  l  e.  ZZ )
154 uzid 11202 . . . . . . . . . . . . 13  |-  ( l  e.  ZZ  ->  l  e.  ( ZZ>= `  l )
)
155153, 154syl 17 . . . . . . . . . . . 12  |-  ( l  e.  NN  ->  l  e.  ( ZZ>= `  l )
)
156 simpr 467 . . . . . . . . . . . . . 14  |-  ( ( l  e.  NN  /\  n  =  l )  ->  n  =  l )
157156fveq2d 5892 . . . . . . . . . . . . 13  |-  ( ( l  e.  NN  /\  n  =  l )  ->  ( F `  n
)  =  ( F `
 l ) )
158157breq2d 4428 . . . . . . . . . . . 12  |-  ( ( l  e.  NN  /\  n  =  l )  ->  ( y  <  ( F `  n )  <->  y  <  ( F `  l ) ) )
159155, 158rspcdv 3165 . . . . . . . . . . 11  |-  ( l  e.  NN  ->  ( A. n  e.  ( ZZ>=
`  l ) y  <  ( F `  n )  ->  y  <  ( F `  l
) ) )
160159reximia 2865 . . . . . . . . . 10  |-  ( E. l  e.  NN  A. n  e.  ( ZZ>= `  l ) y  < 
( F `  n
)  ->  E. l  e.  NN  y  <  ( F `  l )
)
161152, 160syl 17 . . . . . . . . 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 767 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  y  e.  RR )
16390ad2antrr 737 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\ 
A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e. 
dom 
~~>  )  /\  y  e.  RR )  /\  l  e.  NN )  ->  l  e.  NN )
165163, 164ffvelrnd 6046 . . . . . . . . . . . . 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 3442 . . . . . . . . . . . 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 9748 . . . . . . . . . . . 12  |-  ( ( y  e.  RR  /\  ( F `  l )  e.  RR )  -> 
( y  <  ( F `  l )  ->  y  <_  ( F `  l ) ) )
168162, 166, 167syl2anc 671 . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . . 16  |-  ( n  =  l  ->  (
1 ... n )  =  ( 1 ... l
) )
171 esumeq1 28904 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... n )  =  ( 1 ... l )  -> Σ* k  e.  ( 1 ... n ) A  = Σ* k  e.  ( 1 ... l ) A )
172170, 171syl 17 . . . . . . . . . . . . . . 15  |-  ( n  =  l  -> Σ* k  e.  ( 1 ... n ) A  = Σ* k  e.  ( 1 ... l ) A )
173172adantl 472 . . . . . . . . . . . . . 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 28899 . . . . . . . . . . . . . . 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 5977 . . . . . . . . . . . . 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 12218 . . . . . . . . . . . . . 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 781 . . . . . . . . . . . . . . 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 11857 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... l )  ->  k  e.  NN )
180179adantl 472 . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . 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 28945 . . . . . . . . . . . . 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 2496 . . . . . . . . . . . 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 4428 . . . . . . . . . . 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 222 . . . . . . . . . 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 2874 . . . . . . . . 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 11868 . . . . . . . . . . . . . 14  |-  ( 1 ... l )  C_  ( ZZ>= `  1 )
189188, 1sseqtr4i 3477 . . . . . . . . . . . . 13  |-  ( 1 ... l )  C_  NN
190 ovex 6343 . . . . . . . . . . . . . 14  |-  ( 1 ... l )  e. 
_V
191190elpw 3969 . . . . . . . . . . . . 13  |-  ( ( 1 ... l )  e.  ~P NN  <->  ( 1 ... l )  C_  NN )
192189, 191mpbir 214 . . . . . . . . . . . 12  |-  ( 1 ... l )  e. 
~P NN
193 fzfi 12217 . . . . . . . . . . . 12  |-  ( 1 ... l )  e. 
Fin
194 elin 3629 . . . . . . . . . . . 12  |-  ( ( 1 ... l )  e.  ( ~P NN  i^i  Fin )  <->  ( (
1 ... l )  e. 
~P NN  /\  (
1 ... l )  e. 
Fin ) )
195192, 193, 194mpbir2an 936 . . . . . . . . . . 11  |-  ( 1 ... l )  e.  ( ~P NN  i^i  Fin )
196 sumex 13803 . . . . . . . . . . 11  |-  sum_ k  e.  ( 1 ... l
) A  e.  _V
197 eqid 2462 . . . . . . . . . . . 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 13804 . . . . . . . . . . . 12  |-  ( x  =  ( 1 ... l )  ->  sum_ k  e.  x  A  =  sum_ k  e.  ( 1 ... l ) A )
199197, 198elrnmpt1s 5101 . . . . . . . . . . 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 683 . . . . . . . . . 10  |-  sum_ k  e.  ( 1 ... l
) A  e.  ran  ( x  e.  ( ~P NN  i^i  Fin )  |-> 
sum_ k  e.  x  A )
201 nfv 1772 . . . . . . . . . . 11  |-  F/ z  y  <_  sum_ k  e.  ( 1 ... l
) A
202 breq2 4420 . . . . . . . . . . 11  |-  ( z  =  sum_ k  e.  ( 1 ... l ) A  ->  ( y  <_  z  <->  y  <_  sum_ k  e.  ( 1 ... l
) A ) )
203201, 202rspce 3157 . . . . . . . . . 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 681 . . . . . . . . 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 2888 . . . . . . . 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 17 . . . . . . 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 2814 . . . . . 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 467 . . . . . . . . . . 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 3442 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  /\  x  e.  ( ~P NN  i^i  Fin ) )  ->  x  e.  Fin )
210139adantllr 730 . . . . . . . . . . 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 3442 . . . . . . . . . 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 13849 . . . . . . . . 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 9716 . . . . . . . 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 6069 . . . . . . 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 5758 . . . . . . 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 11634 . . . . . . 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 18 . . . . . 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 215 . . . . 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 2496 . . . 4  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  -> Σ* k  e.  NN A  = +oo )
220125, 219breqtrrd 4443 . . 3  |-  ( ( ( ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo ) )  /\  -.  F  e.  dom  ~~>  )  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
22189, 220pm2.61dan 805 . 2  |-  ( (
ph  /\  A. m  e.  NN  B  e.  ( 0 [,) +oo )
)  ->  F ( ~~> t `  J )Σ* k  e.  NN A )
22216reseq1i 5120 . . . . . . . 8  |-  ( F  |`  ( ZZ>= `  k )
)  =  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
)
223 eleq1 2528 . . . . . . . . . . . 12  |-  ( l  =  k  ->  (
l  e.  NN  <->  k  e.  NN ) )
224223anbi2d 715 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( ph  /\  l  e.  NN )  <->  ( ph  /\  k  e.  NN ) ) )
225 sbequ12r 2095 . . . . . . . . . . 11  |-  ( l  =  k  ->  ( [ l  /  k ] A  = +oo  <->  A  = +oo ) )
226224, 225anbi12d 722 . . . . . . . . . 10  |-  ( l  =  k  ->  (
( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo ) 
<->  ( ( ph  /\  k  e.  NN )  /\  A  = +oo ) ) )
227 fveq2 5888 . . . . . . . . . . . 12  |-  ( l  =  k  ->  ( ZZ>=
`  l )  =  ( ZZ>= `  k )
)
228227reseq2d 5124 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  l )
)  =  ( ( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
) )
229227xpeq1d 4876 . . . . . . . . . . 11  |-  ( l  =  k  ->  (
( ZZ>= `  l )  X.  { +oo } )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )
230228, 229eqeq12d 2477 . . . . . . . . . 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 326 . . . . . . . . 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 1772 . . . . . . . . . . . . . 14  |-  F/ k ( ph  /\  l  e.  NN )
233 nfs1v 2277 . . . . . . . . . . . . . 14  |-  F/ k [ l  /  k ] A  = +oo
234232, 233nfan 2022 . . . . . . . . . . . . 13  |-  F/ k ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )
235 nfv 1772 . . . . . . . . . . . . 13  |-  F/ k  n  e.  ( ZZ>= `  l )
236234, 235nfan 2022 . . . . . . . . . . . 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 781 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  ph )
23918adantl 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  k  e.  NN )
240238, 239, 41syl2anc 671 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  / 
k ] A  = +oo )  /\  n  e.  ( ZZ>= `  l )
)  /\  k  e.  ( 1 ... n
) )  ->  A  e.  ( 0 [,] +oo ) )
241 simpllr 774 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  l  e.  NN )
242 elnnuz 11224 . . . . . . . . . . . . . . 15  |-  ( l  e.  NN  <->  l  e.  ( ZZ>= `  1 )
)
243 eluzfz 11824 . . . . . . . . . . . . . . 15  |-  ( ( l  e.  ( ZZ>= ` 
1 )  /\  n  e.  ( ZZ>= `  l )
)  ->  l  e.  ( 1 ... n
) )
244242, 243sylanb 479 . . . . . . . . . . . . . 14  |-  ( ( l  e.  NN  /\  n  e.  ( ZZ>= `  l ) )  -> 
l  e.  ( 1 ... n ) )
245241, 244sylancom 678 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  l  e.  ( 1 ... n ) )
246 simplr 767 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  [ l  / 
k ] A  = +oo )
247 sbequ12 2094 . . . . . . . . . . . . . 14  |-  ( k  =  l  ->  ( A  = +oo  <->  [ l  /  k ] A  = +oo ) )
248233, 247rspce 3157 . . . . . . . . . . . . 13  |-  ( ( l  e.  ( 1 ... n )  /\  [ l  /  k ] A  = +oo )  ->  E. k  e.  ( 1 ... n ) A  = +oo )
249245, 246, 248syl2anc 671 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  ->  E. k  e.  ( 1 ... n ) A  = +oo )
250236, 237, 240, 249esumpinfval 28943 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  l  e.  NN )  /\  [ l  /  k ] A  = +oo )  /\  n  e.  (
ZZ>= `  l ) )  -> Σ* k  e.  ( 1 ... n ) A  = +oo )
251250ralrimiva 2814 . . . . . . . . . 10  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  A. n  e.  (
ZZ>= `  l )Σ* k  e.  ( 1 ... n
) A  = +oo )
252 eqidd 2463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  ( ZZ>= `  l )  =  ( ZZ>= `  l
) )
253 mpteq12 4496 . . . . . . . . . . . 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 478 . . . . . . . . . . 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 767 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  l  e.  NN )  /\  [
l  /  k ] A  = +oo )  ->  l  e.  NN )
256 uznnssnn 11235 . . . . . . . . . . . . 13  |-  ( l  e.  NN  ->  ( ZZ>=
`  l )  C_  NN )
257 resmpt 5173 . . . . . . . . . . . . 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 18 . . . . . . . . . . . 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 471 . . . . . . . . . . 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 4897 . . . . . . . . . . . 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 2506 . . . . . . . . . 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 679 . . . . . . . . 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 2118 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN )  /\  A  = +oo )  ->  (
( n  e.  NN  |-> Σ* k  e.  ( 1 ... n
) A )  |`  ( ZZ>= `  k )
)  =  ( (
ZZ>= `  k )  X. 
{ +oo } ) )
265222, 264syl5eq 2508 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN )  /\  A  = +oo )  ->  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )
266265ex 440 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( A  = +oo  ->  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) ) )
267266reximdva 2874 . . . . 5  |-  ( ph  ->  ( E. k  e.  NN  A  = +oo  ->  E. k  e.  NN  ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } ) ) )
268267imp 435 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  E. k  e.  NN  ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } ) )
269 xrge0topn 28798 . . . . . . . . . . 11  |-  ( TopOpen `  ( RR*ss  ( 0 [,] +oo ) ) )  =  ( (ordTop `  <_  )t  ( 0 [,] +oo )
)
27029, 269eqtri 2484 . . . . . . . . . 10  |-  J  =  ( (ordTop `  <_  )t  ( 0 [,] +oo )
)
271 letopon 20270 . . . . . . . . . . 11  |-  (ordTop `  <_  )  e.  (TopOn `  RR* )
272 iccssxr 11746 . . . . . . . . . . 11  |-  ( 0 [,] +oo )  C_  RR*
273 resttopon 20226 . . . . . . . . . . 11  |-  ( ( (ordTop `  <_  )  e.  (TopOn `  RR* )  /\  ( 0 [,] +oo )  C_  RR* )  ->  (
(ordTop `  <_  )t  ( 0 [,] +oo ) )  e.  (TopOn `  (
0 [,] +oo )
) )
274271, 272, 273mp2an 683 . . . . . . . . . 10  |-  ( (ordTop `  <_  )t  ( 0 [,] +oo ) )  e.  (TopOn `  ( 0 [,] +oo ) )
275270, 274eqeltri 2536 . . . . . . . . 9  |-  J  e.  (TopOn `  ( 0 [,] +oo ) )
276275a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  J  e.  (TopOn `  ( 0 [,] +oo ) ) )
277 0xr 9713 . . . . . . . . . 10  |-  0  e.  RR*
278 pnfxr 11441 . . . . . . . . . 10  |- +oo  e.  RR*
279 0lepnf 11462 . . . . . . . . . 10  |-  0  <_ +oo
280 ubicc2 11778 . . . . . . . . . 10  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  -> +oo  e.  ( 0 [,] +oo ) )
281277, 278, 279, 280mp3an 1373 . . . . . . . . 9  |- +oo  e.  ( 0 [,] +oo )
282281a1i 11 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  -> +oo  e.  ( 0 [,] +oo ) )
28340nnzd 11068 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
284 eqid 2462 . . . . . . . . 9  |-  ( ZZ>= `  k )  =  (
ZZ>= `  k )
285284lmconst 20326 . . . . . . . 8  |-  ( ( J  e.  (TopOn `  ( 0 [,] +oo ) )  /\ +oo  e.  ( 0 [,] +oo )  /\  k  e.  ZZ )  ->  ( ( ZZ>= `  k )  X.  { +oo } ) ( ~~> t `  J ) +oo )
286276, 282, 283, 285syl3anc 1276 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( (
ZZ>= `  k )  X. 
{ +oo } ) ( ~~> t `  J ) +oo )
287 breq1 4419 . . . . . . . 8  |-  ( ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } )  ->  ( ( F  |`  ( ZZ>= `  k
) ) ( ~~> t `  J ) +oo  <->  ( ( ZZ>=
`  k )  X. 
{ +oo } ) ( ~~> t `  J ) +oo ) )
288287biimprd 231 . . . . . . 7  |-  ( ( F  |`  ( ZZ>= `  k ) )  =  ( ( ZZ>= `  k
)  X.  { +oo } )  ->  ( (
( ZZ>= `  k )  X.  { +oo } ) ( ~~> t `  J
) +oo  ->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
)
289286, 288mpan9 476 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )  ->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
290276elfvexd 5916 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 0 [,] +oo )  e. 
_V )
291 cnex 9646 . . . . . . . . . 10  |-  CC  e.  _V
292291a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  CC  e.  _V )
29356adantr 471 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  F : NN
--> ( 0 [,] +oo ) )
294 nnsscn 10642 . . . . . . . . . 10  |-  NN  C_  CC
295294a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  NN  C_  CC )
296 elpm2r 7515 . . . . . . . . 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 1277 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  F  e.  ( ( 0 [,] +oo )  ^pm  CC ) )
298276, 297, 283lmres 20365 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( F ( ~~> t `  J
) +oo  <->  ( F  |`  ( ZZ>= `  k )
) ( ~~> t `  J ) +oo )
)
299298biimpar 492 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) ) ( ~~> t `  J ) +oo )  ->  F ( ~~> t `  J ) +oo )
300289, 299syldan 477 . . . . 5  |-  ( ( ( ph  /\  k  e.  NN )  /\  ( F  |`  ( ZZ>= `  k
) )  =  ( ( ZZ>= `  k )  X.  { +oo } ) )  ->  F ( ~~> t `  J ) +oo )
301300r19.29an 2943 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  ( F  |`  ( ZZ>= `  k )
)  =  ( (
ZZ>= `  k )  X. 
{ +oo } ) )  ->  F ( ~~> t `  J ) +oo )
302268, 301syldan 477 . . 3  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  F ( ~~> t `  J ) +oo )
303 nfv 1772 . . . . 5  |-  F/ k
ph
304 nfre1 2860 . . . . 5  |-  F/ k E. k  e.  NN  A  = +oo
305303, 304nfan 2022 . . . 4  |-  F/ k ( ph  /\  E. k  e.  NN  A  = +oo )
306128a1i 11 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  NN  e.  _V )
30741adantlr 726 . . . 4  |-  ( ( ( ph  /\  E. k  e.  NN  A  = +oo )  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )
308 simpr 467 . . . 4  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  E. k  e.  NN  A  = +oo )
309305, 306, 307, 308esumpinfval 28943 . . 3  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  -> Σ* k  e.  NN A  = +oo )
310302, 309breqtrrd 4443 . 2  |-  ( (
ph  /\  E. k  e.  NN  A  = +oo )  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
311 eleq1 2528 . . . . . . . . 9  |-  ( k  =  m  ->  (
k  e.  NN  <->  m  e.  NN ) )
312311anbi2d 715 . . . . . . . 8  |-  ( k  =  m  ->  (
( ph  /\  k  e.  NN )  <->  ( ph  /\  m  e.  NN ) ) )
3137eleq1d 2524 . . . . . . . 8  |-  ( k  =  m  ->  ( A  e.  ( 0 [,] +oo )  <->  B  e.  ( 0 [,] +oo ) ) )
314312, 313imbi12d 326 . . . . . . 7  |-  ( k  =  m  ->  (
( ( ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,] +oo ) )  <-> 
( ( ph  /\  m  e.  NN )  ->  B  e.  ( 0 [,] +oo ) ) ) )
315314, 41chvarv 2118 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  B  e.  ( 0 [,] +oo ) )
316 eliccelico 28408 . . . . . . 7  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR*  /\  0  <_ +oo )  ->  ( B  e.  ( 0 [,] +oo )  <->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) ) )
317277, 278, 279, 316mp3an 1373 . . . . . 6  |-  ( B  e.  ( 0 [,] +oo )  <->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) )
318315, 317sylib 201 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( B  e.  ( 0 [,) +oo )  \/  B  = +oo ) )
319318ralrimiva 2814 . . . 4  |-  ( ph  ->  A. m  e.  NN  ( B  e.  (
0 [,) +oo )  \/  B  = +oo ) )
320 r19.30 2947 . . . 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 17 . . 3  |-  ( ph  ->  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  \/  E. m  e.  NN  B  = +oo )
)
3227eqeq1d 2464 . . . . 5  |-  ( k  =  m  ->  ( A  = +oo  <->  B  = +oo ) )
323322cbvrexv 3032 . . . 4  |-  ( E. k  e.  NN  A  = +oo  <->  E. m  e.  NN  B  = +oo )
324323orbi2i 526 . . 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 217 . 2  |-  ( ph  ->  ( A. m  e.  NN  B  e.  ( 0 [,) +oo )  \/  E. k  e.  NN  A  = +oo )
)
326221, 310, 325mpjaodan 800 1  |-  ( ph  ->  F ( ~~> t `  J )Σ* k  e.  NN A
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991    = wceq 1455   [wsb 1808    e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057    i^i cin 3415    C_ wss 3416   ~Pcpw 3963   {csn 3980   class class class wbr 4416    |-> cmpt 4475    X. cxp 4851   dom cdm 4853   ran crn 4854    |` cres 4855    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315    ^pm cpm 7499   Fincfn 7595   supcsup 7980   CCcc 9563   RRcr 9564   0cc0 9565   1c1 9566    + caddc 9568   +oocpnf 9698   RR*cxr 9700    < clt 9701    <_ cle 9702   NNcn 10637   ZZcz 10966   ZZ>=cuz 11188   [,)cico 11666   [,]cicc 11667   ...cfz 11813    seqcseq 12245    ~~> cli 13597   sum_csu 13801   ↾s cress 15171   ↾t crest 15368   TopOpenctopn 15369    gsumg cgsu 15388  ordTopcordt 15446   RR*scxrs 15447  ℂfldccnfld 19019  TopOnctopon 19967   ~~> tclm 20291  Σ*cesum 28897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643  ax-addf 9644  ax-mulf 9645
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-fi 7951  df-sup 7982  df-inf 7983  df-oi 8051  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-fzo 11947  df-fl 12060  df-mod 12129  df-seq 12246  df-exp 12305  df-fac 12492  df-bc 12520  df-hash 12548  df-shft 13179  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-limsup 13575  df-clim 13601  df-rlim 13602  df-sum 13802  df-ef 14170  df-sin 14172  df-cos 14173  df-pi 14175  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-starv 15254  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-unif 15262  df-hom 15263  df-cco 15264  df-rest 15370  df-topn 15371  df-0g 15389  df-gsum 15390  df-topgen 15391  df-pt 15392  df-prds 15395  df-ordt 15448  df-xrs 15449  df-qtop 15455  df-imas 15456  df-xps 15459  df-mre 15541  df-mrc 15542  df-acs 15544  df-ps 16495  df-tsr 16496  df-plusf 16536  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-mhm 16631  df-submnd 16632  df-grp 16722  df-minusg 16723  df-sbg 16724  df-mulg 16725  df-subg 16863  df-cntz 17020  df-cmn 17481  df-abl 17482  df-mgp 17773  df-ur 17785  df-ring 17831  df-cring 17832  df-subrg 18055  df-abv 18094  df-lmod 18142  df-scaf 18143  df-sra 18444  df-rgmod 18445  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-fbas 19016  df-fg 19017  df-cnfld 19020  df-top 19970  df-bases 19971  df-topon 19972  df-topsp 19973  df-cld 20083  df-ntr 20084  df-cls 20085  df-nei 20163  df-lp 20201  df-perf 20202  df-cn 20292  df-cnp 20293  df-lm 20294  df-haus 20380  df-tx 20626  df-hmeo 20819  df-fil 20910  df-fm 21002  df-flim 21003  df-flf 21004  df-tmd 21136  df-tgp 21137  df-tsms 21190  df-trg 21223  df-xms 21384  df-ms 21385  df-tms 21386  df-nm 21646  df-ngp 21647  df-nrg 21649  df-nlm 21650  df-ii 21958  df-cncf 21959  df-limc 22870  df-dv 22871  df-log 23555  df-esum 28898
This theorem is referenced by:  esumcvg2  28957
  Copyright terms: Public domain W3C validator