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

Metamath Proof Explorer

Theorem isumdivc

Description: An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006) (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 ∈ ℂ
isumdivc.7 ⊢ φ → B ≠ 0
Assertion isumdivc ⊢ φ → ∑ 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 isumdivc.7 ⊢ φ → B ≠ 0
8 6 7 reccld ⊢ φ → 1 B ∈ ℂ
9 1 2 3 4 5 8 isummulc1 ⊢ φ → ∑ k ∈ Z A ⁢ 1 B = ∑ k ∈ Z A ⁢ 1 B
10 1 2 3 4 5 isumcl ⊢ φ → ∑ k ∈ Z A ∈ ℂ
11 10 6 7 divrecd ⊢ φ → ∑ k ∈ Z A B = ∑ k ∈ Z A ⁢ 1 B
12 6 adantr ⊢ φ ∧ k ∈ Z → B ∈ ℂ
13 7 adantr ⊢ φ ∧ k ∈ Z → B ≠ 0
14 4 12 13 divrecd ⊢ φ ∧ k ∈ Z → A B = A ⁢ 1 B
15 14 sumeq2dv ⊢ φ → ∑ k ∈ Z A B = ∑ k ∈ Z A ⁢ 1 B
16 9 11 15 3eqtr4d ⊢ φ → ∑ k ∈ Z A B = ∑ k ∈ Z A B