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

Metamath Proof Explorer

Theorem isummulc2

Proof