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

Metamath Proof Explorer

Theorem fsumcvg2

Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses fsumsers.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
fsumsers.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fsumsers.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
fsumsers.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion fsumcvg2 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fsumsers.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 fsumsers.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 fsumsers.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 fsumsers.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
5 nfcv ⊢ Ⅎ 𝑚 if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 )
6 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ 𝐴
7 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵
8 nfcv ⊢ Ⅎ 𝑘 0
9 6 7 8 nfif ⊢ Ⅎ 𝑘 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 , 0 )
10 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴 ) )
11 csbeq1a ⊢ ( 𝑘 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
12 10 11 ifbieq1d ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 , 0 ) )
13 5 9 12 cbvmpt ⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑚 ∈ ℤ ↦ if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 , 0 ) )
14 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
15 7 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ
16 11 eleq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
17 15 16 rspc ⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
18 14 17 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∈ ℂ )
19 13 18 2 4 fsumcvg ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ) ⇝ ( seq 𝑀 ( + , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ) ‘ 𝑁 ) )
20 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
21 2 20 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
22 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
23 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
25 24 3 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
26 25 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) )
27 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
28 0cn ⊢ 0 ∈ ℂ
29 27 28 eqeltrdi ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
30 26 29 pm2.61d1 ⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
31 eqid ⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
32 31 fvmpt2 ⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
33 22 30 32 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
34 1 33 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) )
36 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 )
37 36 nfeq2 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑛 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 )
38 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
39 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 ) )
40 38 39 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑛 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 ) ) )
41 37 40 rspc ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑘 ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 ) ) )
42 35 41 mpan9 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ‘ 𝑛 ) )
43 21 42 seqfeq ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( + , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ) )
44 43 fveq1d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ) ) ‘ 𝑁 ) )
45 19 43 44 3brtr4d ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )