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 ⊢ Z = ℤ ≥ M
isumcl.2 ⊢ φ → M ∈ ℤ
isumcl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumcl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
isumcl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
summulc.6 ⊢ φ → B ∈ ℂ
Assertion isummulc1 ⊢ φ → ∑ k ∈ Z A ⁢ B = ∑ k ∈ Z A ⁢ B

Proof

Step Hyp Ref Expression
1 isumcl.1 ⊢ Z = ℤ ≥ M
2 isumcl.2 ⊢ φ → M ∈ ℤ
3 isumcl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
4 isumcl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℂ
5 isumcl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
6 summulc.6 ⊢ φ → B ∈ ℂ
7 1 2 3 4 5 6 isummulc2 ⊢ φ → B ⁢ ∑ k ∈ Z A = ∑ k ∈ Z B ⁢ A
8 1 2 3 4 5 isumcl ⊢ φ → ∑ k ∈ Z A ∈ ℂ
9 8 6 mulcomd ⊢ φ → ∑ k ∈ Z A ⁢ B = B ⁢ ∑ k ∈ Z A
10 6 adantr ⊢ φ ∧ k ∈ Z → B ∈ ℂ
11 4 10 mulcomd ⊢ φ ∧ k ∈ Z → A ⁢ B = B ⁢ A
12 11 sumeq2dv ⊢ φ → ∑ k ∈ Z A ⁢ B = ∑ k ∈ Z B ⁢ A
13 7 9 12 3eqtr4d ⊢ φ → ∑ k ∈ Z A ⁢ B = ∑ k ∈ Z A ⁢ B