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