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 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )