This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isumclim3

Description: The sequence of partial finite sums of a converging infinite series converges to the infinite sum of the series. Note that j must not occur in A . (Contributed by NM, 9-Jan-2006) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumclim3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumclim3.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumclim3.3 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
isumclim3.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isumclim3.5 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 )
Assertion isumclim3 ( 𝜑 → 𝐹 ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )

Proof

Step Hyp Ref Expression
1 isumclim3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumclim3.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isumclim3.3 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
4 isumclim3.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5 isumclim3.5 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 )
6 climdm ⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
7 3 6 sylib ⊢ ( 𝜑 → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8 sumfc ⊢ Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝑍 𝐴
9 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
10 4 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ℂ )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
12 1 2 9 11 isum ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) )
13 8 12 eqtr3id ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) )
14 seqex ⊢ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ∈ V
15 14 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ∈ V )
16 fvres ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
17 fzssuz ⊢ ( 𝑀 ... 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 )
18 17 1 sseqtrri ⊢ ( 𝑀 ... 𝑗 ) ⊆ 𝑍
19 resmpt ⊢ ( ( 𝑀 ... 𝑗 ) ⊆ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) )
20 18 19 ax-mp ⊢ ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 )
21 20 fveq1i ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ↾ ( 𝑀 ... 𝑗 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 )
22 16 21 eqtr3di ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 ) )
23 22 sumeq2i ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 )
24 sumfc ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴
25 23 24 eqtri ⊢ Σ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴
26 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
28 27 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
29 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝜑 )
30 elfzuz ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 30 1 eleqtrrdi ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑗 ) → 𝑚 ∈ 𝑍 )
32 29 31 11 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
33 26 28 32 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → Σ 𝑚 ∈ ( 𝑀 ... 𝑗 ) ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) )
34 25 33 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) 𝐴 = ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) )
35 5 34 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
36 1 15 3 2 35 climeq ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 ↔ 𝐹 ⇝ 𝑥 ) )
37 36 iotabidv ⊢ ( 𝜑 → ( ℩ 𝑥 seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 ) = ( ℩ 𝑥 𝐹 ⇝ 𝑥 ) )
38 df-fv ⊢ ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) = ( ℩ 𝑥 seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝑥 )
39 df-fv ⊢ ( ⇝ ‘ 𝐹 ) = ( ℩ 𝑥 𝐹 ⇝ 𝑥 )
40 37 38 39 3eqtr4g ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ) = ( ⇝ ‘ 𝐹 ) )
41 13 40 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ 𝐹 ) )
42 7 41 breqtrrd ⊢ ( 𝜑 → 𝐹 ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )