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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑚 ) ∈ ℂ )
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	⊢ ( 𝜑 → 𝐹 ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )