isummulc2

Description: An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 23-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	$⊢ Z = ℤ_{\geq M}$
2		isumcl.2	$⊢ φ \to M \in ℤ$
3		isumcl.3	$⊢ (φ \land k \in Z) \to F (k) = A$
4		isumcl.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		isumcl.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
6		summulc.6	$⊢ φ \to B \in ℂ$
7		eqidd	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ B A) (m) = (k \in Z ⟼ B A) (m)$
8	6	adantr	$⊢ (φ \land k \in Z) \to B \in ℂ$
9	8 4	mulcld	$⊢ (φ \land k \in Z) \to B A \in ℂ$
10	9	fmpttd	$⊢ φ \to (k \in Z ⟼ B A) : Z ⟶ ℂ$
11	10	ffvelrnda	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ B A) (m) \in ℂ$
12	1 2 3 4 5	isumclim2	$⊢ φ \to seq M (+ F) ⇝ \sum_{k \in Z} A$
13	3 4	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
14	13	ralrimiva	$⊢ φ \to \forall k \in Z F (k) \in ℂ$
15		fveq2	$⊢ k = m \to F (k) = F (m)$
16	15	eleq1d	$⊢ k = m \to (F (k) \in ℂ \leftrightarrow F (m) \in ℂ)$
17	16	rspccva	$⊢ (\forall k \in Z F (k) \in ℂ \land m \in Z) \to F (m) \in ℂ$
18	14 17	sylan	$⊢ (φ \land m \in Z) \to F (m) \in ℂ$
19		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
20		ovex	$⊢ B A \in V$
21		eqid	$⊢ (k \in Z ⟼ B A) = (k \in Z ⟼ B A)$
22	21	fvmpt2	$⊢ (k \in Z \land B A \in V) \to (k \in Z ⟼ B A) (k) = B A$
23	19 20 22	sylancl	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ B A) (k) = B A$
24	3	oveq2d	$⊢ (φ \land k \in Z) \to B F (k) = B A$
25	23 24	eqtr4d	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ B A) (k) = B F (k)$
26	25	ralrimiva	$⊢ φ \to \forall k \in Z (k \in Z ⟼ B A) (k) = B F (k)$
27		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in Z ⟼ B A) (m)$
28	27	nfeq1	$⊢ Ⅎ k (k \in Z ⟼ B A) (m) = B F (m)$
29		fveq2	$⊢ k = m \to (k \in Z ⟼ B A) (k) = (k \in Z ⟼ B A) (m)$
30	15	oveq2d	$⊢ k = m \to B F (k) = B F (m)$
31	29 30	eqeq12d	$⊢ k = m \to ((k \in Z ⟼ B A) (k) = B F (k) \leftrightarrow (k \in Z ⟼ B A) (m) = B F (m))$
32	28 31	rspc	$⊢ m \in Z \to (\forall k \in Z (k \in Z ⟼ B A) (k) = B F (k) \to (k \in Z ⟼ B A) (m) = B F (m))$
33	26 32	mpan9	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ B A) (m) = B F (m)$
34	1 2 6 12 18 33	isermulc2	$⊢ φ \to seq M (+ (k \in Z ⟼ B A)) ⇝ B \sum_{k \in Z} A$
35	1 2 7 11 34	isumclim	$⊢ φ \to \sum_{m \in Z} (k \in Z ⟼ B A) (m) = B \sum_{k \in Z} A$
36		sumfc	$⊢ \sum_{m \in Z} (k \in Z ⟼ B A) (m) = \sum_{k \in Z} B A$
37	35 36	eqtr3di	$⊢ φ \to B \sum_{k \in Z} A = \sum_{k \in Z} B A$

Metamath Proof Explorer

Theorem isummulc2

Proof