isumadd

Description: Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	isumadd.1	$⊢ Z = ℤ_{\geq M}$
	isumadd.2	$⊢ φ \to M \in ℤ$
	isumadd.3	$⊢ (φ \land k \in Z) \to F (k) = A$
	isumadd.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
	isumadd.5	$⊢ (φ \land k \in Z) \to G (k) = B$
	isumadd.6	$⊢ (φ \land k \in Z) \to B \in ℂ$
	isumadd.7	$⊢ φ \to seq M (+ F) \in dom ⇝$
	isumadd.8	$⊢ φ \to seq M (+ G) \in dom ⇝$
Assertion	isumadd	$⊢ φ \to \sum_{k \in Z} (A + B) = \sum_{k \in Z} A + \sum_{k \in Z} B$

Proof

Step	Hyp	Ref	Expression
1		isumadd.1	$⊢ Z = ℤ_{\geq M}$
2		isumadd.2	$⊢ φ \to M \in ℤ$
3		isumadd.3	$⊢ (φ \land k \in Z) \to F (k) = A$
4		isumadd.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		isumadd.5	$⊢ (φ \land k \in Z) \to G (k) = B$
6		isumadd.6	$⊢ (φ \land k \in Z) \to B \in ℂ$
7		isumadd.7	$⊢ φ \to seq M (+ F) \in dom ⇝$
8		isumadd.8	$⊢ φ \to seq M (+ G) \in dom ⇝$
9		fveq2	$⊢ m = k \to F (m) = F (k)$
10		fveq2	$⊢ m = k \to G (m) = G (k)$
11	9 10	oveq12d	$⊢ m = k \to F (m) + G (m) = F (k) + G (k)$
12		eqid	$⊢ (m \in Z ⟼ F (m) + G (m)) = (m \in Z ⟼ F (m) + G (m))$
13		ovex	$⊢ F (k) + G (k) \in V$
14	11 12 13	fvmpt	$⊢ k \in Z \to (m \in Z ⟼ F (m) + G (m)) (k) = F (k) + G (k)$
15	14	adantl	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ F (m) + G (m)) (k) = F (k) + G (k)$
16	3 5	oveq12d	$⊢ (φ \land k \in Z) \to F (k) + G (k) = A + B$
17	15 16	eqtrd	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ F (m) + G (m)) (k) = A + B$
18	4 6	addcld	$⊢ (φ \land k \in Z) \to A + B \in ℂ$
19	1 2 3 4 7	isumclim2	$⊢ φ \to seq M (+ F) ⇝ \sum_{k \in Z} A$
20		seqex	$⊢ seq M (+ (m \in Z ⟼ F (m) + G (m))) \in V$
21	20	a1i	$⊢ φ \to seq M (+ (m \in Z ⟼ F (m) + G (m))) \in V$
22	1 2 5 6 8	isumclim2	$⊢ φ \to seq M (+ G) ⇝ \sum_{k \in Z} B$
23	3 4	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
24	1 2 23	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
25	24	ffvelrnda	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ℂ$
26	5 6	eqeltrd	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
27	1 2 26	serf	$⊢ φ \to seq M (+ G) : Z ⟶ ℂ$
28	27	ffvelrnda	$⊢ (φ \land j \in Z) \to seq M (+ G) (j) \in ℂ$
29		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
30	29 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
31		simpll	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to φ$
32		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
33	32 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
34	33	adantl	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to k \in Z$
35	31 34 23	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℂ$
36	31 34 26	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to G (k) \in ℂ$
37	34 14	syl	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to (m \in Z ⟼ F (m) + G (m)) (k) = F (k) + G (k)$
38	30 35 36 37	seradd	$⊢ (φ \land j \in Z) \to seq M (+ (m \in Z ⟼ F (m) + G (m))) (j) = seq M (+ F) (j) + seq M (+ G) (j)$
39	1 2 19 21 22 25 28 38	climadd	$⊢ φ \to seq M (+ (m \in Z ⟼ F (m) + G (m))) ⇝ (\sum_{k \in Z} A + \sum_{k \in Z} B)$
40	1 2 17 18 39	isumclim	$⊢ φ \to \sum_{k \in Z} (A + B) = \sum_{k \in Z} A + \sum_{k \in Z} B$

Metamath Proof Explorer

Theorem isumadd

Proof