isermulc2

Description: Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007) (Revised by Mario Carneiro, 1-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$⊢ Z = ℤ_{\geq M}$
2		isermulc2.2	$⊢ φ \to M \in ℤ$
3		isermulc2.4	$⊢ φ \to C \in ℂ$
4		isermulc2.5	$⊢ φ \to seq M (+ F) ⇝ A$
5		isermulc2.6	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
6		isermulc2.7	$⊢ (φ \land k \in Z) \to G (k) = C F (k)$
7		seqex	$⊢ seq M (+ G) \in V$
8	7	a1i	$⊢ φ \to seq M (+ G) \in V$
9	1 2 5	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
10	9	ffvelcdmda	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ℂ$
11		addcl	$⊢ (k \in ℂ \land x \in ℂ) \to k + x \in ℂ$
12	11	adantl	$⊢ ((φ \land j \in Z) \land (k \in ℂ \land x \in ℂ)) \to k + x \in ℂ$
13	3	adantr	$⊢ (φ \land j \in Z) \to C \in ℂ$
14		adddi	$⊢ (C \in ℂ \land k \in ℂ \land x \in ℂ) \to C (k + x) = C k + C x$
15	14	3expb	$⊢ (C \in ℂ \land (k \in ℂ \land x \in ℂ)) \to C (k + x) = C k + C x$
16	13 15	sylan	$⊢ ((φ \land j \in Z) \land (k \in ℂ \land x \in ℂ)) \to C (k + x) = C k + C x$
17		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
18	17 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
19		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
20	19 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
21	20 5	sylan2	$⊢ (φ \land k \in (M \dots j)) \to F (k) \in ℂ$
22	21	adantlr	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℂ$
23	20 6	sylan2	$⊢ (φ \land k \in (M \dots j)) \to G (k) = C F (k)$
24	23	adantlr	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to G (k) = C F (k)$
25	12 16 18 22 24	seqdistr	$⊢ (φ \land j \in Z) \to seq M (+ G) (j) = C seq M (+ F) (j)$
26	1 2 4 3 8 10 25	climmulc2	$⊢ φ \to seq M (+ G) ⇝ C A$

Metamath Proof Explorer

Theorem isermulc2

Proof