Theorem isummulc1

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

	Ref	Expression
Hypotheses	isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
	summulc.6	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	isummulc1	⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		isumcl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6		summulc.6	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	1 2 3 4 5 6	isummulc2	⊢ ( 𝜑 → ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )
8	1 2 3 4 5	isumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )
9	8 6	mulcomd	⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 · 𝐵 ) = ( 𝐵 · Σ 𝑘 ∈ 𝑍 𝐴 ) )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
11	4 10	mulcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
12	11	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐵 · 𝐴 ) )
13	7 9 12	3eqtr4d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) )