Metamath Proof Explorer

Theorem sge0isummpt2

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0isummpt2.kph 
|- F/ k ph
sge0isummpt2.a 
|- ( ( ph /\ k e. Z ) -> A e. ( 0 [,) +oo ) )
sge0isummpt2.m 
|- ( ph -> M e. ZZ )
sge0isummpt2.z 
|- Z = ( ZZ>= ` M )
sge0isummpt2.b 
|- ( ph -> seq M ( + , ( k e. Z |-> A ) ) ~~> B )
Assertion sge0isummpt2 
|- ( ph -> ( sum^ ` ( k e. Z |-> A ) ) = sum_ k e. Z A )

Proof

Step Hyp Ref Expression
1 sge0isummpt2.kph 
 |-  F/ k ph
2 sge0isummpt2.a 
 |-  ( ( ph /\ k e. Z ) -> A e. ( 0 [,) +oo ) )
3 sge0isummpt2.m 
 |-  ( ph -> M e. ZZ )
4 sge0isummpt2.z 
 |-  Z = ( ZZ>= ` M )
5 sge0isummpt2.b 
 |-  ( ph -> seq M ( + , ( k e. Z |-> A ) ) ~~> B )
6 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
7 nfv 
 |-  F/ k j e. Z
8 1 7 nfan 
 |-  F/ k ( ph /\ j e. Z )
9 nfcv 
 |-  F/_ k j
10 9 nfcsb1 
 |-  F/_ k [_ j / k ]_ A
11 10 nfel1 
 |-  F/ k [_ j / k ]_ A e. ( 0 [,) +oo )
12 8 11 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. ( 0 [,) +oo ) )
13 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
14 13 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
15 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
16 15 eleq1d 
 |-  ( k = j -> ( A e. ( 0 [,) +oo ) <-> [_ j / k ]_ A e. ( 0 [,) +oo ) ) )
17 14 16 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> A e. ( 0 [,) +oo ) ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. ( 0 [,) +oo ) ) ) )
18 12 17 2 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. ( 0 [,) +oo ) )
19 nfcv 
 |-  F/_ i A
20 nfcsb1v 
 |-  F/_ k [_ i / k ]_ A
21 csbeq1a 
 |-  ( k = i -> A = [_ i / k ]_ A )
22 19 20 21 cbvmpt 
 |-  ( k e. Z |-> A ) = ( i e. Z |-> [_ i / k ]_ A )
23 22 eqcomi 
 |-  ( i e. Z |-> [_ i / k ]_ A ) = ( k e. Z |-> A )
24 9 10 15 23 fvmptf 
 |-  ( ( j e. Z /\ [_ j / k ]_ A e. ( 0 [,) +oo ) ) -> ( ( i e. Z |-> [_ i / k ]_ A ) ` j ) = [_ j / k ]_ A )
25 6 18 24 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( i e. Z |-> [_ i / k ]_ A ) ` j ) = [_ j / k ]_ A )
26 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
27 ax-resscn 
 |-  RR C_ CC
28 26 27 sstri 
 |-  ( 0 [,) +oo ) C_ CC
29 28 18 sselid 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC )
30 22 a1i 
 |-  ( ph -> ( k e. Z |-> A ) = ( i e. Z |-> [_ i / k ]_ A ) )
31 30 seqeq3d 
 |-  ( ph -> seq M ( + , ( k e. Z |-> A ) ) = seq M ( + , ( i e. Z |-> [_ i / k ]_ A ) ) )
32 31 breq1d 
 |-  ( ph -> ( seq M ( + , ( k e. Z |-> A ) ) ~~> B <-> seq M ( + , ( i e. Z |-> [_ i / k ]_ A ) ) ~~> B ) )
33 5 32 mpbid 
 |-  ( ph -> seq M ( + , ( i e. Z |-> [_ i / k ]_ A ) ) ~~> B )
34 4 3 25 29 33 isumclim 
 |-  ( ph -> sum_ j e. Z [_ j / k ]_ A = B )
35 nfcv 
 |-  F/_ j Z
36 nfcv 
 |-  F/_ k Z
37 nfcv 
 |-  F/_ j A
38 15 35 36 37 10 cbvsum 
 |-  sum_ k e. Z A = sum_ j e. Z [_ j / k ]_ A
39 38 a1i 
 |-  ( ph -> sum_ k e. Z A = sum_ j e. Z [_ j / k ]_ A )
40 1 2 3 4 5 sge0isummpt 
 |-  ( ph -> ( sum^ ` ( k e. Z |-> A ) ) = B )
41 34 39 40 3eqtr4rd 
 |-  ( ph -> ( sum^ ` ( k e. Z |-> A ) ) = sum_ k e. Z A )