fsumcvg

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	summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
	summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	sumrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
	fsumcvg.4	$⊢ φ \to A \subseteq (M \dots N)$
Assertion	fsumcvg	$⊢ φ \to seq M (+ F) ⇝ seq M (+ F) (N)$

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		sumrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		fsumcvg.4	$⊢ φ \to A \subseteq (M \dots N)$
5		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
6		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
7	3 6	syl	$⊢ φ \to N \in ℤ$
8		seqex	$⊢ seq M (+ F) \in V$
9	8	a1i	$⊢ φ \to seq M (+ F) \in V$
10		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	3 11	syl	$⊢ φ \to M \in ℤ$
13		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
14		iftrue	$⊢ k \in A \to if (k \in A, B, 0) = B$
15	14	adantl	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) = B$
16	15 2	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) \in ℂ$
17	16	ex	$⊢ φ \to (k \in A \to if (k \in A, B, 0) \in ℂ)$
18		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 0) = 0$
19		0cn	$⊢ 0 \in ℂ$
20	18 19	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 0) \in ℂ$
21	17 20	pm2.61d1	$⊢ φ \to if (k \in A, B, 0) \in ℂ$
22	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 0) \in ℂ) \to F (k) = if (k \in A, B, 0)$
23	13 21 22	syl2anr	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = if (k \in A, B, 0)$
24	21	adantr	$⊢ (φ \land k \in ℤ_{\geq M}) \to if (k \in A, B, 0) \in ℂ$
25	23 24	eqeltrd	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) \in ℂ$
26	10 12 25	serf	$⊢ φ \to seq M (+ F) : ℤ_{\geq M} ⟶ ℂ$
27	26 3	ffvelrnd	$⊢ φ \to seq M (+ F) (N) \in ℂ$
28		addid1	$⊢ m \in ℂ \to m + 0 = m$
29	28	adantl	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℂ) \to m + 0 = m$
30	3	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to N \in ℤ_{\geq M}$
31		simpr	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in ℤ_{\geq N}$
32	27	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (+ F) (N) \in ℂ$
33		elfzuz	$⊢ m \in (N + 1 \dots n) \to m \in ℤ_{\geq (N + 1)}$
34		eluzelz	$⊢ m \in ℤ_{\geq (N + 1)} \to m \in ℤ$
35	34	adantl	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to m \in ℤ$
36	4	sseld	$⊢ φ \to (m \in A \to m \in (M \dots N))$
37		fznuz	$⊢ m \in (M \dots N) \to \neg m \in ℤ_{\geq (N + 1)}$
38	36 37	syl6	$⊢ φ \to (m \in A \to \neg m \in ℤ_{\geq (N + 1)})$
39	38	con2d	$⊢ φ \to (m \in ℤ_{\geq (N + 1)} \to \neg m \in A)$
40	39	imp	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to \neg m \in A$
41	35 40	eldifd	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to m \in (ℤ ∖ A)$
42		fveqeq2	$⊢ k = m \to (F (k) = 0 \leftrightarrow F (m) = 0)$
43		eldifi	$⊢ k \in (ℤ ∖ A) \to k \in ℤ$
44		eldifn	$⊢ k \in (ℤ ∖ A) \to \neg k \in A$
45	44 18	syl	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 0) = 0$
46	45 19	eqeltrdi	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 0) \in ℂ$
47	43 46 22	syl2anc	$⊢ k \in (ℤ ∖ A) \to F (k) = if (k \in A, B, 0)$
48	47 45	eqtrd	$⊢ k \in (ℤ ∖ A) \to F (k) = 0$
49	42 48	vtoclga	$⊢ m \in (ℤ ∖ A) \to F (m) = 0$
50	41 49	syl	$⊢ (φ \land m \in ℤ_{\geq (N + 1)}) \to F (m) = 0$
51	33 50	sylan2	$⊢ (φ \land m \in (N + 1 \dots n)) \to F (m) = 0$
52	51	adantlr	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in (N + 1 \dots n)) \to F (m) = 0$
53	29 30 31 32 52	seqid2	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (+ F) (N) = seq M (+ F) (n)$
54	53	eqcomd	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (+ F) (n) = seq M (+ F) (N)$
55	5 7 9 27 54	climconst	$⊢ φ \to seq M (+ F) ⇝ seq M (+ F) (N)$

Metamath Proof Explorer

Theorem fsumcvg

Proof