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	$⊢ Z = ℤ_{\geq M}$
	climfsum.2	$⊢ φ \to M \in ℤ$
	climfsum.3	$⊢ φ \to A \in Fin$
	climfsum.5	$⊢ (φ \land k \in A) \to F ⇝ B$
	climfsum.6	$⊢ φ \to H \in W$
	climfsum.7	$⊢ (φ \land (k \in A \land n \in Z)) \to F (n) \in ℂ$
	climfsum.8	$⊢ (φ \land n \in Z) \to H (n) = \sum_{k \in A} F (n)$
Assertion	climfsum	$⊢ φ \to H ⇝ \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		climfsum.1	$⊢ Z = ℤ_{\geq M}$
2		climfsum.2	$⊢ φ \to M \in ℤ$
3		climfsum.3	$⊢ φ \to A \in Fin$
4		climfsum.5	$⊢ (φ \land k \in A) \to F ⇝ B$
5		climfsum.6	$⊢ φ \to H \in W$
6		climfsum.7	$⊢ (φ \land (k \in A \land n \in Z)) \to F (n) \in ℂ$
7		climfsum.8	$⊢ (φ \land n \in Z) \to H (n) = \sum_{k \in A} F (n)$
8	7	mpteq2dva	$⊢ φ \to (n \in Z ⟼ H (n)) = (n \in Z ⟼ \sum_{k \in A} F (n))$
9		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
10	1 9	eqsstri	$⊢ Z \subseteq ℤ$
11		zssre	$⊢ ℤ \subseteq ℝ$
12	10 11	sstri	$⊢ Z \subseteq ℝ$
13	12	a1i	$⊢ φ \to Z \subseteq ℝ$
14		fvexd	$⊢ (φ \land (n \in Z \land k \in A)) \to F (n) \in V$
15	2	adantr	$⊢ (φ \land k \in A) \to M \in ℤ$
16		climrel	$⊢ Rel ⇝$
17	16	brrelex1i	$⊢ F ⇝ B \to F \in V$
18	4 17	syl	$⊢ (φ \land k \in A) \to F \in V$
19		eqid	$⊢ (n \in Z ⟼ F (n)) = (n \in Z ⟼ F (n))$
20	1 19	climmpt	$⊢ (M \in ℤ \land F \in V) \to (F ⇝ B \leftrightarrow (n \in Z ⟼ F (n)) ⇝ B)$
21	15 18 20	syl2anc	$⊢ (φ \land k \in A) \to (F ⇝ B \leftrightarrow (n \in Z ⟼ F (n)) ⇝ B)$
22	4 21	mpbid	$⊢ (φ \land k \in A) \to (n \in Z ⟼ F (n)) ⇝ B$
23	6	anassrs	$⊢ ((φ \land k \in A) \land n \in Z) \to F (n) \in ℂ$
24	23	fmpttd	$⊢ (φ \land k \in A) \to (n \in Z ⟼ F (n)) : Z ⟶ ℂ$
25	1 15 24	rlimclim	$⊢ (φ \land k \in A) \to ((n \in Z ⟼ F (n)) \underset{ℝ}{⇝} B \leftrightarrow (n \in Z ⟼ F (n)) ⇝ B)$
26	22 25	mpbird	$⊢ (φ \land k \in A) \to (n \in Z ⟼ F (n)) \underset{ℝ}{⇝} B$
27	13 3 14 26	fsumrlim	$⊢ φ \to (n \in Z ⟼ \sum_{k \in A} F (n)) \underset{ℝ}{⇝} \sum_{k \in A} B$
28	3	adantr	$⊢ (φ \land n \in Z) \to A \in Fin$
29	6	anass1rs	$⊢ ((φ \land n \in Z) \land k \in A) \to F (n) \in ℂ$
30	28 29	fsumcl	$⊢ (φ \land n \in Z) \to \sum_{k \in A} F (n) \in ℂ$
31	30	fmpttd	$⊢ φ \to (n \in Z ⟼ \sum_{k \in A} F (n)) : Z ⟶ ℂ$
32	1 2 31	rlimclim	$⊢ φ \to ((n \in Z ⟼ \sum_{k \in A} F (n)) \underset{ℝ}{⇝} \sum_{k \in A} B \leftrightarrow (n \in Z ⟼ \sum_{k \in A} F (n)) ⇝ \sum_{k \in A} B)$
33	27 32	mpbid	$⊢ φ \to (n \in Z ⟼ \sum_{k \in A} F (n)) ⇝ \sum_{k \in A} B$
34	8 33	eqbrtrd	$⊢ φ \to (n \in Z ⟼ H (n)) ⇝ \sum_{k \in A} B$
35		eqid	$⊢ (n \in Z ⟼ H (n)) = (n \in Z ⟼ H (n))$
36	1 35	climmpt	$⊢ (M \in ℤ \land H \in W) \to (H ⇝ \sum_{k \in A} B \leftrightarrow (n \in Z ⟼ H (n)) ⇝ \sum_{k \in A} B)$
37	2 5 36	syl2anc	$⊢ φ \to (H ⇝ \sum_{k \in A} B \leftrightarrow (n \in Z ⟼ H (n)) ⇝ \sum_{k \in A} B)$
38	34 37	mpbird	$⊢ φ \to H ⇝ \sum_{k \in A} B$

Metamath Proof Explorer

Theorem climfsum

Proof