This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 · 𝐵 ) )