Theorem climfsum

Description: Limit of a finite sum of converging sequences. Note that F ( k ) is a collection of functions with implicit parameter k , each of which converges to B ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-Jul-2014) (Proof shortened by Mario Carneiro, 22-May-2016)

	Ref	Expression
Hypotheses	climfsum.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climfsum.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climfsum.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	climfsum.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐹 ⇝ 𝐵 )
	climfsum.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
	climfsum.7	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑛 ∈ 𝑍 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
	climfsum.8	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) )
Assertion	climfsum	⊢ ( 𝜑 → 𝐻 ⇝ Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		climfsum.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climfsum.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climfsum.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		climfsum.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐹 ⇝ 𝐵 )
5		climfsum.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
6		climfsum.7	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑛 ∈ 𝑍 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
7		climfsum.8	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) )
8	7	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) )
9		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
10	1 9	eqsstri	⊢ 𝑍 ⊆ ℤ
11		zssre	⊢ ℤ ⊆ ℝ
12	10 11	sstri	⊢ 𝑍 ⊆ ℝ
13	12	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
14		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ V )
15	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
16		climrel	⊢ Rel ⇝
17	16	brrelex1i	⊢ ( 𝐹 ⇝ 𝐵 → 𝐹 ∈ V )
18	4 17	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐹 ∈ V )
19		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) )
20	1 19	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ V ) → ( 𝐹 ⇝ 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐵 ) )
21	15 18 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ⇝ 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐵 ) )
22	4 21	mpbid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐵 )
23	6	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
24	23	fmpttd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) : 𝑍 ⟶ ℂ )
25	1 15 24	rlimclim	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐵 ) )
26	22 25	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐵 )
27	13 3 14 26	fsumrlim	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 Σ 𝑘 ∈ 𝐴 𝐵 )
28	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐴 ∈ Fin )
29	6	anass1rs	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
30	28 29	fsumcl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
31	30	fmpttd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) : 𝑍 ⟶ ℂ )
32	1 2 31	rlimclim	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 Σ 𝑘 ∈ 𝐴 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) ⇝ Σ 𝑘 ∈ 𝐴 𝐵 ) )
33	27 32	mpbid	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑛 ) ) ⇝ Σ 𝑘 ∈ 𝐴 𝐵 )
34	8 33	eqbrtrd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) ) ⇝ Σ 𝑘 ∈ 𝐴 𝐵 )
35		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) )
36	1 35	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐻 ∈ 𝑊 ) → ( 𝐻 ⇝ Σ 𝑘 ∈ 𝐴 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) ) ⇝ Σ 𝑘 ∈ 𝐴 𝐵 ) )
37	2 5 36	syl2anc	⊢ ( 𝜑 → ( 𝐻 ⇝ Σ 𝑘 ∈ 𝐴 𝐵 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑛 ) ) ⇝ Σ 𝑘 ∈ 𝐴 𝐵 ) )
38	34 37	mpbird	⊢ ( 𝜑 → 𝐻 ⇝ Σ 𝑘 ∈ 𝐴 𝐵 )