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	$⊢ Z = ℤ_{\geq M}$
	isumclim3.2	$⊢ φ \to M \in ℤ$
	isumclim3.3	$⊢ φ \to F \in dom ⇝$
	isumclim3.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
	isumclim3.5	$⊢ (φ \land j \in Z) \to F (j) = \sum_{k = M}^{j} A$
Assertion	isumclim3	$⊢ φ \to F ⇝ \sum_{k \in Z} A$

Proof

Step	Hyp	Ref	Expression
1		isumclim3.1	$⊢ Z = ℤ_{\geq M}$
2		isumclim3.2	$⊢ φ \to M \in ℤ$
3		isumclim3.3	$⊢ φ \to F \in dom ⇝$
4		isumclim3.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		isumclim3.5	$⊢ (φ \land j \in Z) \to F (j) = \sum_{k = M}^{j} A$
6		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
7	3 6	sylib	$⊢ φ \to F ⇝ ⇝ (F)$
8		sumfc	$⊢ \sum_{m \in Z} (k \in Z ⟼ A) (m) = \sum_{k \in Z} A$
9		eqidd	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (m)$
10	4	fmpttd	$⊢ φ \to (k \in Z ⟼ A) : Z ⟶ ℂ$
11	10	ffvelcdmda	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ A) (m) \in ℂ$
12	1 2 9 11	isum	$⊢ φ \to \sum_{m \in Z} (k \in Z ⟼ A) (m) = ⇝ (seq M (+ (k \in Z ⟼ A)))$
13	8 12	eqtr3id	$⊢ φ \to \sum_{k \in Z} A = ⇝ (seq M (+ (k \in Z ⟼ A)))$
14		seqex	$⊢ seq M (+ (k \in Z ⟼ A)) \in V$
15	14	a1i	$⊢ φ \to seq M (+ (k \in Z ⟼ A)) \in V$
16		fvres	$⊢ m \in (M \dots j) \to ({(k \in Z ⟼ A) ↾}_{(M \dots j)}) (m) = (k \in Z ⟼ A) (m)$
17		fzssuz	$⊢ (M \dots j) \subseteq ℤ_{\geq M}$
18	17 1	sseqtrri	$⊢ (M \dots j) \subseteq Z$
19		resmpt	$⊢ (M \dots j) \subseteq Z \to {(k \in Z ⟼ A) ↾}_{(M \dots j)} = (k \in (M \dots j) ⟼ A)$
20	18 19	ax-mp	$⊢ {(k \in Z ⟼ A) ↾}_{(M \dots j)} = (k \in (M \dots j) ⟼ A)$
21	20	fveq1i	$⊢ ({(k \in Z ⟼ A) ↾}_{(M \dots j)}) (m) = (k \in (M \dots j) ⟼ A) (m)$
22	16 21	eqtr3di	$⊢ m \in (M \dots j) \to (k \in Z ⟼ A) (m) = (k \in (M \dots j) ⟼ A) (m)$
23	22	sumeq2i	$⊢ \sum_{m = M}^{j} (k \in Z ⟼ A) (m) = \sum_{m = M}^{j} (k \in (M \dots j) ⟼ A) (m)$
24		sumfc	$⊢ \sum_{m = M}^{j} (k \in (M \dots j) ⟼ A) (m) = \sum_{k = M}^{j} A$
25	23 24	eqtri	$⊢ \sum_{m = M}^{j} (k \in Z ⟼ A) (m) = \sum_{k = M}^{j} A$
26		eqidd	$⊢ ((φ \land j \in Z) \land m \in (M \dots j)) \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (m)$
27		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
28	27 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
29		simpl	$⊢ (φ \land j \in Z) \to φ$
30		elfzuz	$⊢ m \in (M \dots j) \to m \in ℤ_{\geq M}$
31	30 1	eleqtrrdi	$⊢ m \in (M \dots j) \to m \in Z$
32	29 31 11	syl2an	$⊢ ((φ \land j \in Z) \land m \in (M \dots j)) \to (k \in Z ⟼ A) (m) \in ℂ$
33	26 28 32	fsumser	$⊢ (φ \land j \in Z) \to \sum_{m = M}^{j} (k \in Z ⟼ A) (m) = seq M (+ (k \in Z ⟼ A)) (j)$
34	25 33	eqtr3id	$⊢ (φ \land j \in Z) \to \sum_{k = M}^{j} A = seq M (+ (k \in Z ⟼ A)) (j)$
35	5 34	eqtr2d	$⊢ (φ \land j \in Z) \to seq M (+ (k \in Z ⟼ A)) (j) = F (j)$
36	1 15 3 2 35	climeq	$⊢ φ \to (seq M (+ (k \in Z ⟼ A)) ⇝ x \leftrightarrow F ⇝ x)$
37	36	iotabidv	$⊢ φ \to (ι x \| seq M (+ (k \in Z ⟼ A)) ⇝ x) = (ι x \| F ⇝ x)$
38		df-fv	$⊢ ⇝ (seq M (+ (k \in Z ⟼ A))) = (ι x \| seq M (+ (k \in Z ⟼ A)) ⇝ x)$
39		df-fv	$⊢ ⇝ (F) = (ι x \| F ⇝ x)$
40	37 38 39	3eqtr4g	$⊢ φ \to ⇝ (seq M (+ (k \in Z ⟼ A))) = ⇝ (F)$
41	13 40	eqtrd	$⊢ φ \to \sum_{k \in Z} A = ⇝ (F)$
42	7 41	breqtrrd	$⊢ φ \to F ⇝ \sum_{k \in Z} A$

Metamath Proof Explorer

Theorem isumclim3

Proof