Theorem 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isermulc2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isermulc2.4	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	isermulc2.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
	isermulc2.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	isermulc2.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
Assertion	isermulc2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ ( 𝐶 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isermulc2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isermulc2.4	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		isermulc2.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
5		isermulc2.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6		isermulc2.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
7		seqex	⊢ seq 𝑀 ( + , 𝐺 ) ∈ V
8	7	a1i	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ V )
9	1 2 5	serf	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
10	9	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
11		addcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
12	11	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐶 ∈ ℂ )
14		adddi	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
15	14	3expb	⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
16	13 15	sylan	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝐶 · ( 𝑘 + 𝑥 ) ) = ( ( 𝐶 · 𝑘 ) + ( 𝐶 · 𝑥 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
18	17 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
19		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20	19 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
21	20 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
22	21	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
23	20 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
24	23	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
25	12 16 18 22 24	seqdistr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) = ( 𝐶 · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) )
26	1 2 4 3 8 10 25	climmulc2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ ( 𝐶 · 𝐴 ) )