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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumcl.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumcl.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumcl.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isumcl.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
summulc.6 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
isumdivc.7 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion isumdivc ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 / 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 / 𝐵 ) )

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 isumdivc.7 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
8 6 7 reccld ⊢ ( 𝜑 → ( 1 / 𝐵 ) ∈ ℂ )
9 1 2 3 4 5 8 isummulc1 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 · ( 1 / 𝐵 ) ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 · ( 1 / 𝐵 ) ) )
10 1 2 3 4 5 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℂ )
11 10 6 7 divrecd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 / 𝐵 ) = ( Σ 𝑘 ∈ 𝑍 𝐴 · ( 1 / 𝐵 ) ) )
12 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ≠ 0 )
14 4 12 13 divrecd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
15 14 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( 𝐴 / 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 · ( 1 / 𝐵 ) ) )
16 9 11 15 3eqtr4d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝑍 𝐴 / 𝐵 ) = Σ 𝑘 ∈ 𝑍 ( 𝐴 / 𝐵 ) )