Metamath Proof Explorer

Theorem fsumsermpt

Description: A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses fsumsermpt.m 
|- ( ph -> M e. ZZ )
fsumsermpt.z 
|- Z = ( ZZ>= ` M )
fsumsermpt.a 
|- ( ( ph /\ k e. Z ) -> A e. CC )
fsumsermpt.f 
|- F = ( n e. Z |-> sum_ k e. ( M ... n ) A )
fsumsermpt.g 
|- G = seq M ( + , ( k e. Z |-> A ) )
Assertion fsumsermpt 
|- ( ph -> F = G )

Proof

Step Hyp Ref Expression
1 fsumsermpt.m 
 |-  ( ph -> M e. ZZ )
2 fsumsermpt.z 
 |-  Z = ( ZZ>= ` M )
3 fsumsermpt.a 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
4 fsumsermpt.f 
 |-  F = ( n e. Z |-> sum_ k e. ( M ... n ) A )
5 fsumsermpt.g 
 |-  G = seq M ( + , ( k e. Z |-> A ) )
6 fzfid 
 |-  ( ph -> ( M ... m ) e. Fin )
7 simpl 
 |-  ( ( ph /\ k e. ( M ... m ) ) -> ph )
8 elfzuz 
 |-  ( k e. ( M ... m ) -> k e. ( ZZ>= ` M ) )
9 8 2 eleqtrrdi 
 |-  ( k e. ( M ... m ) -> k e. Z )
10 9 adantl 
 |-  ( ( ph /\ k e. ( M ... m ) ) -> k e. Z )
11 7 10 3 syl2anc 
 |-  ( ( ph /\ k e. ( M ... m ) ) -> A e. CC )
12 6 11 fsumcl 
 |-  ( ph -> sum_ k e. ( M ... m ) A e. CC )
13 12 adantr 
 |-  ( ( ph /\ m e. Z ) -> sum_ k e. ( M ... m ) A e. CC )
14 13 ralrimiva 
 |-  ( ph -> A. m e. Z sum_ k e. ( M ... m ) A e. CC )
15 oveq2 
 |-  ( n = m -> ( M ... n ) = ( M ... m ) )
16 15 sumeq1d 
 |-  ( n = m -> sum_ k e. ( M ... n ) A = sum_ k e. ( M ... m ) A )
17 16 cbvmptv 
 |-  ( n e. Z |-> sum_ k e. ( M ... n ) A ) = ( m e. Z |-> sum_ k e. ( M ... m ) A )
18 4 17 eqtri 
 |-  F = ( m e. Z |-> sum_ k e. ( M ... m ) A )
19 18 fnmpt 
 |-  ( A. m e. Z sum_ k e. ( M ... m ) A e. CC -> F Fn Z )
20 14 19 syl 
 |-  ( ph -> F Fn Z )
21 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
22 nfv 
 |-  F/ k ( ph /\ j e. Z )
23 nfcv 
 |-  F/_ k j
24 23 nfcsb1 
 |-  F/_ k [_ j / k ]_ A
25 24 nfel1 
 |-  F/ k [_ j / k ]_ A e. CC
26 22 25 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC )
27 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
28 27 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
29 csbeq1a 
 |-  ( k = j -> A = [_ j / k ]_ A )
30 29 eleq1d 
 |-  ( k = j -> ( A e. CC <-> [_ j / k ]_ A e. CC ) )
31 28 30 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> A e. CC ) <-> ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC ) ) )
32 26 31 3 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> [_ j / k ]_ A e. CC )
33 eqid 
 |-  ( k e. Z |-> A ) = ( k e. Z |-> A )
34 23 24 29 33 fvmptf 
 |-  ( ( j e. Z /\ [_ j / k ]_ A e. CC ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
35 21 32 34 syl2anc 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
36 35 32 eqeltrd 
 |-  ( ( ph /\ j e. Z ) -> ( ( k e. Z |-> A ) ` j ) e. CC )
37 addcl 
 |-  ( ( j e. CC /\ x e. CC ) -> ( j + x ) e. CC )
38 37 adantl 
 |-  ( ( ph /\ ( j e. CC /\ x e. CC ) ) -> ( j + x ) e. CC )
39 2 1 36 38 seqf 
 |-  ( ph -> seq M ( + , ( k e. Z |-> A ) ) : Z --> CC )
40 39 ffnd 
 |-  ( ph -> seq M ( + , ( k e. Z |-> A ) ) Fn Z )
41 5 a1i 
 |-  ( ph -> G = seq M ( + , ( k e. Z |-> A ) ) )
42 41 fneq1d 
 |-  ( ph -> ( G Fn Z <-> seq M ( + , ( k e. Z |-> A ) ) Fn Z ) )
43 40 42 mpbird 
 |-  ( ph -> G Fn Z )
44 simpr 
 |-  ( ( ph /\ m e. Z ) -> m e. Z )
45 18 fvmpt2 
 |-  ( ( m e. Z /\ sum_ k e. ( M ... m ) A e. CC ) -> ( F ` m ) = sum_ k e. ( M ... m ) A )
46 44 13 45 syl2anc 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = sum_ k e. ( M ... m ) A )
47 nfcv 
 |-  F/_ j ( M ... m )
48 nfcv 
 |-  F/_ k ( M ... m )
49 nfcv 
 |-  F/_ j A
50 29 47 48 49 24 cbvsum 
 |-  sum_ k e. ( M ... m ) A = sum_ j e. ( M ... m ) [_ j / k ]_ A
51 50 a1i 
 |-  ( ( ph /\ m e. Z ) -> sum_ k e. ( M ... m ) A = sum_ j e. ( M ... m ) [_ j / k ]_ A )
52 46 51 eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = sum_ j e. ( M ... m ) [_ j / k ]_ A )
53 simpl 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> ph )
54 elfzuz 
 |-  ( j e. ( M ... m ) -> j e. ( ZZ>= ` M ) )
55 54 2 eleqtrrdi 
 |-  ( j e. ( M ... m ) -> j e. Z )
56 55 adantl 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> j e. Z )
57 53 56 35 syl2anc 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
58 57 adantlr 
 |-  ( ( ( ph /\ m e. Z ) /\ j e. ( M ... m ) ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
59 id 
 |-  ( m e. Z -> m e. Z )
60 59 2 eleqtrdi 
 |-  ( m e. Z -> m e. ( ZZ>= ` M ) )
61 60 adantl 
 |-  ( ( ph /\ m e. Z ) -> m e. ( ZZ>= ` M ) )
62 53 56 32 syl2anc 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> [_ j / k ]_ A e. CC )
63 62 adantlr 
 |-  ( ( ( ph /\ m e. Z ) /\ j e. ( M ... m ) ) -> [_ j / k ]_ A e. CC )
64 58 61 63 fsumser 
 |-  ( ( ph /\ m e. Z ) -> sum_ j e. ( M ... m ) [_ j / k ]_ A = ( seq M ( + , ( k e. Z |-> A ) ) ` m ) )
65 5 fveq1i 
 |-  ( G ` m ) = ( seq M ( + , ( k e. Z |-> A ) ) ` m )
66 65 eqcomi 
 |-  ( seq M ( + , ( k e. Z |-> A ) ) ` m ) = ( G ` m )
67 66 a1i 
 |-  ( ( ph /\ m e. Z ) -> ( seq M ( + , ( k e. Z |-> A ) ) ` m ) = ( G ` m ) )
68 52 64 67 3eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = ( G ` m ) )
69 20 43 68 eqfnfvd 
 |-  ( ph -> F = G )