isumsplit

Description: Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumsplit.1	$⊢ Z = ℤ_{\geq M}$
	isumsplit.2	$⊢ W = ℤ_{\geq N}$
	isumsplit.3	$⊢ φ \to N \in Z$
	isumsplit.4	$⊢ (φ \land k \in Z) \to F (k) = A$
	isumsplit.5	$⊢ (φ \land k \in Z) \to A \in ℂ$
	isumsplit.6	$⊢ φ \to seq M (+ F) \in dom ⇝$
Assertion	isumsplit	$⊢ φ \to \sum_{k \in Z} A = \sum_{k = M}^{N - 1} A + \sum_{k \in W} A$

Proof

Step	Hyp	Ref	Expression
1		isumsplit.1	$⊢ Z = ℤ_{\geq M}$
2		isumsplit.2	$⊢ W = ℤ_{\geq N}$
3		isumsplit.3	$⊢ φ \to N \in Z$
4		isumsplit.4	$⊢ (φ \land k \in Z) \to F (k) = A$
5		isumsplit.5	$⊢ (φ \land k \in Z) \to A \in ℂ$
6		isumsplit.6	$⊢ φ \to seq M (+ F) \in dom ⇝$
7	3 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
8		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
9	7 8	syl	$⊢ φ \to M \in ℤ$
10		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
11	7 10	syl	$⊢ φ \to N \in ℤ$
12		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
13	7 12	syl	$⊢ φ \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
14	13 2 1	3sstr4g	$⊢ φ \to W \subseteq Z$
15	14	sselda	$⊢ (φ \land k \in W) \to k \in Z$
16	15 4	syldan	$⊢ (φ \land k \in W) \to F (k) = A$
17	15 5	syldan	$⊢ (φ \land k \in W) \to A \in ℂ$
18	4 5	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
19	1 3 18	iserex	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow seq N (+ F) \in dom ⇝)$
20	6 19	mpbid	$⊢ φ \to seq N (+ F) \in dom ⇝$
21	2 11 16 17 20	isumclim2	$⊢ φ \to seq N (+ F) ⇝ \sum_{k \in W} A$
22		fzfid	$⊢ φ \to (M \dots N - 1) \in Fin$
23		elfzuz	$⊢ k \in (M \dots N - 1) \to k \in ℤ_{\geq M}$
24	23 1	eleqtrrdi	$⊢ k \in (M \dots N - 1) \to k \in Z$
25	24 5	sylan2	$⊢ (φ \land k \in (M \dots N - 1)) \to A \in ℂ$
26	22 25	fsumcl	$⊢ φ \to \sum_{k = M}^{N - 1} A \in ℂ$
27	15 18	syldan	$⊢ (φ \land k \in W) \to F (k) \in ℂ$
28	2 11 27	serf	$⊢ φ \to seq N (+ F) : W ⟶ ℂ$
29	28	ffvelcdmda	$⊢ (φ \land j \in W) \to seq N (+ F) (j) \in ℂ$
30	9	zred	$⊢ φ \to M \in ℝ$
31	30	ltm1d	$⊢ φ \to M - 1 < M$
32		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
33		fzn	$⊢ (M \in ℤ \land M - 1 \in ℤ) \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
34	9 32 33	syl2anc2	$⊢ φ \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
35	31 34	mpbid	$⊢ φ \to (M \dots M - 1) = \emptyset$
36	35	sumeq1d	$⊢ φ \to \sum_{k = M}^{M - 1} A = \sum_{k \in \emptyset} A$
37	36	adantr	$⊢ (φ \land j \in W) \to \sum_{k = M}^{M - 1} A = \sum_{k \in \emptyset} A$
38		sum0	$⊢ \sum_{k \in \emptyset} A = 0$
39	37 38	eqtrdi	$⊢ (φ \land j \in W) \to \sum_{k = M}^{M - 1} A = 0$
40	39	oveq1d	$⊢ (φ \land j \in W) \to \sum_{k = M}^{M - 1} A + seq M (+ F) (j) = 0 + seq M (+ F) (j)$
41	14	sselda	$⊢ (φ \land j \in W) \to j \in Z$
42	1 9 18	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
43	42	ffvelcdmda	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ℂ$
44	41 43	syldan	$⊢ (φ \land j \in W) \to seq M (+ F) (j) \in ℂ$
45	44	addlidd	$⊢ (φ \land j \in W) \to 0 + seq M (+ F) (j) = seq M (+ F) (j)$
46	40 45	eqtr2d	$⊢ (φ \land j \in W) \to seq M (+ F) (j) = \sum_{k = M}^{M - 1} A + seq M (+ F) (j)$
47		oveq1	$⊢ N = M \to N - 1 = M - 1$
48	47	oveq2d	$⊢ N = M \to (M \dots N - 1) = (M \dots M - 1)$
49	48	sumeq1d	$⊢ N = M \to \sum_{k = M}^{N - 1} A = \sum_{k = M}^{M - 1} A$
50		seqeq1	$⊢ N = M \to seq N (+ F) = seq M (+ F)$
51	50	fveq1d	$⊢ N = M \to seq N (+ F) (j) = seq M (+ F) (j)$
52	49 51	oveq12d	$⊢ N = M \to \sum_{k = M}^{N - 1} A + seq N (+ F) (j) = \sum_{k = M}^{M - 1} A + seq M (+ F) (j)$
53	52	eqeq2d	$⊢ N = M \to (seq M (+ F) (j) = \sum_{k = M}^{N - 1} A + seq N (+ F) (j) \leftrightarrow seq M (+ F) (j) = \sum_{k = M}^{M - 1} A + seq M (+ F) (j))$
54	46 53	syl5ibrcom	$⊢ (φ \land j \in W) \to (N = M \to seq M (+ F) (j) = \sum_{k = M}^{N - 1} A + seq N (+ F) (j))$
55		addcl	$⊢ (k \in ℂ \land m \in ℂ) \to k + m \in ℂ$
56	55	adantl	$⊢ (((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \land (k \in ℂ \land m \in ℂ)) \to k + m \in ℂ$
57		addass	$⊢ (k \in ℂ \land m \in ℂ \land x \in ℂ) \to k + m + x = k + m + x$
58	57	adantl	$⊢ (((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \land (k \in ℂ \land m \in ℂ \land x \in ℂ)) \to k + m + x = k + m + x$
59		simplr	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to j \in W$
60		simpll	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to φ$
61	11	zcnd	$⊢ φ \to N \in ℂ$
62		ax-1cn	$⊢ 1 \in ℂ$
63		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
64	61 62 63	sylancl	$⊢ φ \to N - 1 + 1 = N$
65	64	eqcomd	$⊢ φ \to N = N - 1 + 1$
66	60 65	syl	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to N = N - 1 + 1$
67	66	fveq2d	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to ℤ_{\geq N} = ℤ_{\geq (N - 1 + 1)}$
68	2 67	eqtrid	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to W = ℤ_{\geq (N - 1 + 1)}$
69	59 68	eleqtrd	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to j \in ℤ_{\geq (N - 1 + 1)}$
70	9	adantr	$⊢ (φ \land j \in W) \to M \in ℤ$
71		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
72	70 71	sylan	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
73		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
74	73 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
75	60 74 18	syl2an	$⊢ (((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots j)) \to F (k) \in ℂ$
76	56 58 69 72 75	seqsplit	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to seq M (+ F) (j) = seq M (+ F) (N - 1) + seq (N - 1 + 1) (+ F) (j)$
77	60 24 4	syl2an	$⊢ (((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to F (k) = A$
78	60 24 5	syl2an	$⊢ (((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to A \in ℂ$
79	77 72 78	fsumser	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M}^{N - 1} A = seq M (+ F) (N - 1)$
80	66	seqeq1d	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to seq N (+ F) = seq (N - 1 + 1) (+ F)$
81	80	fveq1d	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to seq N (+ F) (j) = seq (N - 1 + 1) (+ F) (j)$
82	79 81	oveq12d	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M}^{N - 1} A + seq N (+ F) (j) = seq M (+ F) (N - 1) + seq (N - 1 + 1) (+ F) (j)$
83	76 82	eqtr4d	$⊢ ((φ \land j \in W) \land N \in ℤ_{\geq (M + 1)}) \to seq M (+ F) (j) = \sum_{k = M}^{N - 1} A + seq N (+ F) (j)$
84	83	ex	$⊢ (φ \land j \in W) \to (N \in ℤ_{\geq (M + 1)} \to seq M (+ F) (j) = \sum_{k = M}^{N - 1} A + seq N (+ F) (j))$
85		uzp1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
86	7 85	syl	$⊢ φ \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
87	86	adantr	$⊢ (φ \land j \in W) \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
88	54 84 87	mpjaod	$⊢ (φ \land j \in W) \to seq M (+ F) (j) = \sum_{k = M}^{N - 1} A + seq N (+ F) (j)$
89	2 11 21 26 6 29 88	climaddc2	$⊢ φ \to seq M (+ F) ⇝ (\sum_{k = M}^{N - 1} A + \sum_{k \in W} A)$
90	1 9 4 5 89	isumclim	$⊢ φ \to \sum_{k \in Z} A = \sum_{k = M}^{N - 1} A + \sum_{k \in W} A$

Metamath Proof Explorer

Theorem isumsplit

Proof