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 A
48 29 47 24 cbvsum 
 |-  sum_ k e. ( M ... m ) A = sum_ j e. ( M ... m ) [_ j / k ]_ A
49 48 a1i 
 |-  ( ( ph /\ m e. Z ) -> sum_ k e. ( M ... m ) A = sum_ j e. ( M ... m ) [_ j / k ]_ A )
50 46 49 eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = sum_ j e. ( M ... m ) [_ j / k ]_ A )
51 simpl 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> ph )
52 elfzuz 
 |-  ( j e. ( M ... m ) -> j e. ( ZZ>= ` M ) )
53 52 2 eleqtrrdi 
 |-  ( j e. ( M ... m ) -> j e. Z )
54 53 adantl 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> j e. Z )
55 51 54 35 syl2anc 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
56 55 adantlr 
 |-  ( ( ( ph /\ m e. Z ) /\ j e. ( M ... m ) ) -> ( ( k e. Z |-> A ) ` j ) = [_ j / k ]_ A )
57 id 
 |-  ( m e. Z -> m e. Z )
58 57 2 eleqtrdi 
 |-  ( m e. Z -> m e. ( ZZ>= ` M ) )
59 58 adantl 
 |-  ( ( ph /\ m e. Z ) -> m e. ( ZZ>= ` M ) )
60 51 54 32 syl2anc 
 |-  ( ( ph /\ j e. ( M ... m ) ) -> [_ j / k ]_ A e. CC )
61 60 adantlr 
 |-  ( ( ( ph /\ m e. Z ) /\ j e. ( M ... m ) ) -> [_ j / k ]_ A e. CC )
62 56 59 61 fsumser 
 |-  ( ( ph /\ m e. Z ) -> sum_ j e. ( M ... m ) [_ j / k ]_ A = ( seq M ( + , ( k e. Z |-> A ) ) ` m ) )
63 5 fveq1i 
 |-  ( G ` m ) = ( seq M ( + , ( k e. Z |-> A ) ) ` m )
64 63 eqcomi 
 |-  ( seq M ( + , ( k e. Z |-> A ) ) ` m ) = ( G ` m )
65 64 a1i 
 |-  ( ( ph /\ m e. Z ) -> ( seq M ( + , ( k e. Z |-> A ) ) ` m ) = ( G ` m ) )
66 50 62 65 3eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) = ( G ` m ) )
67 20 43 66 eqfnfvd 
 |-  ( ph -> F = G )