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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fsumsermpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
fsumsermpt.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
fsumsermpt.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 )
fsumsermpt.g ⊢ 𝐺 = seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) )
Assertion fsumsermpt ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 fsumsermpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 fsumsermpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 fsumsermpt.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
4 fsumsermpt.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 )
5 fsumsermpt.g ⊢ 𝐺 = seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) )
6 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑚 ) ∈ Fin )
7 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → 𝜑 )
8 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑚 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 8 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑚 ) → 𝑘 ∈ 𝑍 )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → 𝑘 ∈ 𝑍 )
11 7 10 3 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑚 ) ) → 𝐴 ∈ ℂ )
12 6 11 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 ∈ ℂ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 ∈ ℂ )
14 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 ∈ ℂ )
15 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑚 ) )
16 15 sumeq1d ⊢ ( 𝑛 = 𝑚 → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 )
17 16 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) 𝐴 ) = ( 𝑚 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 )
18 4 17 eqtri ⊢ 𝐹 = ( 𝑚 ∈ 𝑍 ↦ Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 )
19 18 fnmpt ⊢ ( ∀ 𝑚 ∈ 𝑍 Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 ∈ ℂ → 𝐹 Fn 𝑍 )
20 14 19 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
22 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
23 nfcv ⊢ Ⅎ 𝑘 𝑗
24 23 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
25 24 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ
26 22 25 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ )
27 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
28 27 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
29 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
30 29 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
31 28 30 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) ) )
32 26 31 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ )
33 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 )
34 23 24 29 33 fvmptf ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
35 21 32 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
36 35 32 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℂ )
37 addcl ⊢ ( ( 𝑗 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑗 + 𝑥 ) ∈ ℂ )
38 37 adantl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑗 + 𝑥 ) ∈ ℂ )
39 2 1 36 38 seqf ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) : 𝑍 ⟶ ℂ )
40 39 ffnd ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) Fn 𝑍 )
41 5 a1i ⊢ ( 𝜑 → 𝐺 = seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) )
42 41 fneq1d ⊢ ( 𝜑 → ( 𝐺 Fn 𝑍 ↔ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) Fn 𝑍 ) )
43 40 42 mpbird ⊢ ( 𝜑 → 𝐺 Fn 𝑍 )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
45 18 fvmpt2 ⊢ ( ( 𝑚 ∈ 𝑍 ∧ Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 ∈ ℂ ) → ( 𝐹 ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 )
46 44 13 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 )
47 nfcv ⊢ Ⅎ 𝑗 𝐴
48 29 47 24 cbvsum ⊢ Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 = Σ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ⦋ 𝑗 / 𝑘 ⦌ 𝐴
49 48 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑚 ) 𝐴 = Σ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
50 46 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = Σ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
51 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → 𝜑 )
52 elfzuz ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑚 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
53 52 2 eleqtrrdi ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑚 ) → 𝑗 ∈ 𝑍 )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → 𝑗 ∈ 𝑍 )
55 51 54 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
56 55 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
57 id ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ 𝑍 )
58 57 2 eleqtrdi ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
60 51 54 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ )
61 60 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ )
62 56 59 61 fsumser ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → Σ 𝑗 ∈ ( 𝑀 ... 𝑚 ) ⦋ 𝑗 / 𝑘 ⦌ 𝐴 = ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑚 ) )
63 5 fveq1i ⊢ ( 𝐺 ‘ 𝑚 ) = ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑚 )
64 63 eqcomi ⊢ ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 )
65 64 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
66 50 62 65 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
67 20 43 66 eqfnfvd ⊢ ( 𝜑 → 𝐹 = 𝐺 )