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