Metamath Proof Explorer

Theorem fsumcvg

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 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
sumrb.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fsumcvg.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
Assertion fsumcvg ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 sumrb.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 fsumcvg.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑀 ... 𝑁 ) )
5 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
6 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
7 3 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
9 8 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ V )
10 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
11 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12 3 11 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
14 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
16 15 2 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
17 16 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) )
18 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
19 0cn ⊢ 0 ∈ ℂ
20 18 19 eqeltrdi ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
21 17 20 pm2.61d1 ⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
22 1 fvmpt2 ⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
23 13 21 22 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
24 21 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
25 23 24 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
26 10 12 25 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ ℂ )
27 26 3 ffvelrnd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
28 addid1 ⊢ ( 𝑚 ∈ ℂ → ( 𝑚 + 0 ) = 𝑚 )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ℂ ) → ( 𝑚 + 0 ) = 𝑚 )
30 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
32 27 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
33 elfzuz ⊢ ( 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) → 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
34 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → 𝑚 ∈ ℤ )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ℤ )
36 4 sseld ⊢ ( 𝜑 → ( 𝑚 ∈ 𝐴 → 𝑚 ∈ ( 𝑀 ... 𝑁 ) ) )
37 fznuz ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ¬ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
38 36 37 syl6 ⊢ ( 𝜑 → ( 𝑚 ∈ 𝐴 → ¬ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
39 38 con2d ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ¬ 𝑚 ∈ 𝐴 ) )
40 39 imp ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ¬ 𝑚 ∈ 𝐴 )
41 35 40 eldifd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑚 ∈ ( ℤ ∖ 𝐴 ) )
42 fveqeq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) = 0 ↔ ( 𝐹 ‘ 𝑚 ) = 0 ) )
43 eldifi ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → 𝑘 ∈ ℤ )
44 eldifn ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
45 44 18 syl ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
46 45 19 eqeltrdi ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
47 43 46 22 syl2anc ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
48 47 45 eqtrd ⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 0 )
49 42 48 vtoclga ⊢ ( 𝑚 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑚 ) = 0 )
50 41 49 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑚 ) = 0 )
51 33 50 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = 0 )
52 51 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑚 ∈ ( ( 𝑁 + 1 ) ... 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) = 0 )
53 29 30 31 32 52 seqid2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
54 53 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
55 5 7 9 27 54 climconst ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )