Metamath Proof Explorer

Theorem esumcvgsum

Description: The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019)

Ref Expression
Hypotheses esumcvgsum.1 
|- ( k = i -> A = B )
esumcvgsum.2 
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
esumcvgsum.3 
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = A )
esumcvgsum.4 
|- ( ph -> seq 1 ( + , F ) ~~> L )
esumcvgsum.5 
|- ( ph -> L e. RR )
Assertion esumcvgsum 
|- ( ph -> sum* k e. NN A = sum_ k e. NN A )

Proof

Step Hyp Ref Expression
1 esumcvgsum.1 
 |-  ( k = i -> A = B )
2 esumcvgsum.2 
 |-  ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) )
3 esumcvgsum.3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = A )
4 esumcvgsum.4 
 |-  ( ph -> seq 1 ( + , F ) ~~> L )
5 esumcvgsum.5 
 |-  ( ph -> L e. RR )
6 simpll 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> ph )
7 elfznn 
 |-  ( k e. ( 1 ... j ) -> k e. NN )
8 7 adantl 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> k e. NN )
9 6 8 3 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> ( F ` k ) = A )
10 nnuz 
 |-  NN = ( ZZ>= ` 1 )
11 10 eleq2i 
 |-  ( j e. NN <-> j e. ( ZZ>= ` 1 ) )
12 11 bilani 
 |-  ( ( ph /\ j e. NN ) -> j e. ( ZZ>= ` 1 ) )
13 mnfxr 
 |-  -oo e. RR*
14 pnfxr 
 |-  +oo e. RR*
15 0re 
 |-  0 e. RR
16 mnflt 
 |-  ( 0 e. RR -> -oo < 0 )
17 15 16 ax-mp 
 |-  -oo < 0
18 pnfge 
 |-  ( +oo e. RR* -> +oo <_ +oo )
19 14 18 ax-mp 
 |-  +oo <_ +oo
20 icossioo 
 |-  ( ( ( -oo e. RR* /\ +oo e. RR* ) /\ ( -oo < 0 /\ +oo <_ +oo ) ) -> ( 0 [,) +oo ) C_ ( -oo (,) +oo ) )
21 13 14 17 19 20 mp4an 
 |-  ( 0 [,) +oo ) C_ ( -oo (,) +oo )
22 ioomax 
 |-  ( -oo (,) +oo ) = RR
23 21 22 sseqtri 
 |-  ( 0 [,) +oo ) C_ RR
24 6 8 2 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> A e. ( 0 [,) +oo ) )
25 23 24 sselid 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> A e. RR )
26 25 recnd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( 1 ... j ) ) -> A e. CC )
27 9 12 26 fsumser 
 |-  ( ( ph /\ j e. NN ) -> sum_ k e. ( 1 ... j ) A = ( seq 1 ( + , F ) ` j ) )
28 27 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> sum_ k e. ( 1 ... j ) A ) = ( j e. NN |-> ( seq 1 ( + , F ) ` j ) ) )
29 1z 
 |-  1 e. ZZ
30 seqfn 
 |-  ( 1 e. ZZ -> seq 1 ( + , F ) Fn ( ZZ>= ` 1 ) )
31 29 30 ax-mp 
 |-  seq 1 ( + , F ) Fn ( ZZ>= ` 1 )
32 fneq2 
 |-  ( NN = ( ZZ>= ` 1 ) -> ( seq 1 ( + , F ) Fn NN <-> seq 1 ( + , F ) Fn ( ZZ>= ` 1 ) ) )
33 10 32 ax-mp 
 |-  ( seq 1 ( + , F ) Fn NN <-> seq 1 ( + , F ) Fn ( ZZ>= ` 1 ) )
34 31 33 mpbir 
 |-  seq 1 ( + , F ) Fn NN
35 dffn5 
 |-  ( seq 1 ( + , F ) Fn NN <-> seq 1 ( + , F ) = ( j e. NN |-> ( seq 1 ( + , F ) ` j ) ) )
36 34 35 mpbi 
 |-  seq 1 ( + , F ) = ( j e. NN |-> ( seq 1 ( + , F ) ` j ) )
37 seqex 
 |-  seq 1 ( + , F ) e. _V
38 37 a1i 
 |-  ( ph -> seq 1 ( + , F ) e. _V )
39 breldmg 
 |-  ( ( seq 1 ( + , F ) e. _V /\ L e. RR /\ seq 1 ( + , F ) ~~> L ) -> seq 1 ( + , F ) e. dom ~~> )
40 38 5 4 39 syl3anc 
 |-  ( ph -> seq 1 ( + , F ) e. dom ~~> )
41 36 40 eqeltrrid 
 |-  ( ph -> ( j e. NN |-> ( seq 1 ( + , F ) ` j ) ) e. dom ~~> )
42 28 41 eqeltrd 
 |-  ( ph -> ( j e. NN |-> sum_ k e. ( 1 ... j ) A ) e. dom ~~> )
43 2 1 42 esumpcvgval 
 |-  ( ph -> sum* k e. NN A = sum_ k e. NN A )