# 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}={ℤ}_{\ge {M}}$
isumcl.2 ${⊢}{\phi }\to {M}\in ℤ$
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 seq{M}\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}={ℤ}_{\ge {M}}$
2 isumcl.2 ${⊢}{\phi }\to {M}\in ℤ$
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 seq{M}\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)$