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