Theorem fsumdivc

Description: A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsummulc2.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsummulc2.2	$$⊢\phi \to C\in ℂ$$
	fsummulc2.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
	fsumdivc.4	$$⊢\phi \to C\ne 0$$
Assertion	fsumdivc	$$⊢\phi \to \frac{\sum _{k\in A}B}{C}=\sum _{k\in A}\left(\frac{B}{C}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsummulc2.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsummulc2.2	$$⊢\phi \to C\in ℂ$$
3		fsummulc2.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		fsumdivc.4	$$⊢\phi \to C\ne 0$$
5	2 4	reccld	$$⊢\phi \to \frac{1}{C}\in ℂ$$
6	1 5 3	fsummulc1	$$⊢\phi \to \sum _{k\in A}B\left(\frac{1}{C}\right)=\sum _{k\in A}B\left(\frac{1}{C}\right)$$
7	1 3	fsumcl	$$⊢\phi \to \sum _{k\in A}B\in ℂ$$
8	7 2 4	divrecd	$$⊢\phi \to \frac{\sum _{k\in A}B}{C}=\sum _{k\in A}B\left(\frac{1}{C}\right)$$
9	2	adantr	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℂ$$
10	4	adantr	$$⊢\left(\phi \wedge k\in A\right)\to C\ne 0$$
11	3 9 10	divrecd	$$⊢\left(\phi \wedge k\in A\right)\to \frac{B}{C}=B\left(\frac{1}{C}\right)$$
12	11	sumeq2dv	$$⊢\phi \to \sum _{k\in A}\left(\frac{B}{C}\right)=\sum _{k\in A}B\left(\frac{1}{C}\right)$$
13	6 8 12	3eqtr4d	$$⊢\phi \to \frac{\sum _{k\in A}B}{C}=\sum _{k\in A}\left(\frac{B}{C}\right)$$