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={\mathbb{Z}}_{\ge M}$$
	isumcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumcl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
	isumcl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
	summulc.6	$$⊢\phi \to B\in ℂ$$
	isumdivc.7	$$⊢\phi \to B\ne 0$$
Assertion	isumdivc	$$⊢\phi \to \frac{\sum _{k\in Z}A}{B}=\sum _{k\in Z}\left(\frac{A}{B}\right)$$

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumcl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isumcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
5		isumcl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6		summulc.6	$$⊢\phi \to B\in ℂ$$
7		isumdivc.7	$$⊢\phi \to B\ne 0$$
8	6 7	reccld	$$⊢\phi \to \frac{1}{B}\in ℂ$$
9	1 2 3 4 5 8	isummulc1	$$⊢\phi \to \sum _{k\in Z}A\left(\frac{1}{B}\right)=\sum _{k\in Z}A\left(\frac{1}{B}\right)$$
10	1 2 3 4 5	isumcl	$$⊢\phi \to \sum _{k\in Z}A\in ℂ$$
11	10 6 7	divrecd	$$⊢\phi \to \frac{\sum _{k\in Z}A}{B}=\sum _{k\in Z}A\left(\frac{1}{B}\right)$$
12	6	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
13	7	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to B\ne 0$$
14	4 12 13	divrecd	$$⊢\left(\phi \wedge k\in Z\right)\to \frac{A}{B}=A\left(\frac{1}{B}\right)$$
15	14	sumeq2dv	$$⊢\phi \to \sum _{k\in Z}\left(\frac{A}{B}\right)=\sum _{k\in Z}A\left(\frac{1}{B}\right)$$
16	9 11 15	3eqtr4d	$$⊢\phi \to \frac{\sum _{k\in Z}A}{B}=\sum _{k\in Z}\left(\frac{A}{B}\right)$$