Theorem fsumshftm

Description: Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	fsumrev.1	$$⊢\phi \to K\in \mathbb{Z}$$
	fsumrev.2	$$⊢\phi \to M\in \mathbb{Z}$$
	fsumrev.3	$$⊢\phi \to N\in \mathbb{Z}$$
	fsumrev.4	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
	fsumshftm.5	$$⊢j=k+K\to A=B$$
Assertion	fsumshftm	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M-K}^{N-K}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumrev.1	$$⊢\phi \to K\in \mathbb{Z}$$
2		fsumrev.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		fsumrev.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		fsumrev.4	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
5		fsumshftm.5	$$⊢j=k+K\to A=B$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}mA$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋m/j⦌A$$
8		csbeq1a	$$⊢j=m\to A=⦋m/j⦌A$$
9	6 7 8	cbvsumi	$$⊢\sum _{j=M}^{N}A=\sum _{m=M}^N⦋m/j⦌A$$
10	1	znegcld	$$⊢\phi \to -K\in \mathbb{Z}$$
11	4	ralrimiva	$$⊢\phi \to \forall j\in \left(M\dots N\right)A\in ℂ$$
12	7	nfel1	$$⊢Ⅎj⦋m/j⦌A\in ℂ$$
13	8	eleq1d	$$⊢j=m\to \left(A\in ℂ\leftrightarrow ⦋m/j⦌A\in ℂ\right)$$
14	12 13	rspc	$$⊢m\in \left(M\dots N\right)\to \left(\forall j\in \left(M\dots N\right)A\in ℂ\to ⦋m/j⦌A\in ℂ\right)$$
15	11 14	mpan9	$$⊢\left(\phi \wedge m\in \left(M\dots N\right)\right)\to ⦋m/j⦌A\in ℂ$$
16		csbeq1	$$⊢m=k-\left(-K\right)\to ⦋m/j⦌A=⦋\left(k-\left(-K\right)\right)/j⦌A$$
17	10 2 3 15 16	fsumshft	$$⊢\phi \to \sum _{m=M}^N⦋m/j⦌A=\sum _{k=M+\left(-K\right)}^{N+\left(-K\right)}⦋\left(k-\left(-K\right)\right)/j⦌A$$
18	2	zcnd	$$⊢\phi \to M\in ℂ$$
19	1	zcnd	$$⊢\phi \to K\in ℂ$$
20	18 19	negsubd	$$⊢\phi \to M+\left(-K\right)=M-K$$
21	3	zcnd	$$⊢\phi \to N\in ℂ$$
22	21 19	negsubd	$$⊢\phi \to N+\left(-K\right)=N-K$$
23	20 22	oveq12d	$$⊢\phi \to \left(M+\left(-K\right)\dots N+\left(-K\right)\right)=\left(M-K\dots N-K\right)$$
24	23	sumeq1d	$$⊢\phi \to \sum _{k=M+\left(-K\right)}^{N+\left(-K\right)}⦋\left(k-\left(-K\right)\right)/j⦌A=\sum _{k=M-K}^{N-K}⦋\left(k-\left(-K\right)\right)/j⦌A$$
25		elfzelz	$$⊢k\in \left(M-K\dots N-K\right)\to k\in \mathbb{Z}$$
26	25	zcnd	$$⊢k\in \left(M-K\dots N-K\right)\to k\in ℂ$$
27		subneg	$$⊢\left(k\in ℂ\wedge K\in ℂ\right)\to k-\left(-K\right)=k+K$$
28	26 19 27	syl2anr	$$⊢\left(\phi \wedge k\in \left(M-K\dots N-K\right)\right)\to k-\left(-K\right)=k+K$$
29	28	csbeq1d	$$⊢\left(\phi \wedge k\in \left(M-K\dots N-K\right)\right)\to ⦋\left(k-\left(-K\right)\right)/j⦌A=⦋\left(k+K\right)/j⦌A$$
30		ovex	$$⊢k+K\in \mathrm{V}$$
31	30 5	csbie	$$⊢⦋\left(k+K\right)/j⦌A=B$$
32	29 31	eqtrdi	$$⊢\left(\phi \wedge k\in \left(M-K\dots N-K\right)\right)\to ⦋\left(k-\left(-K\right)\right)/j⦌A=B$$
33	32	sumeq2dv	$$⊢\phi \to \sum _{k=M-K}^{N-K}⦋\left(k-\left(-K\right)\right)/j⦌A=\sum _{k=M-K}^{N-K}B$$
34	17 24 33	3eqtrd	$$⊢\phi \to \sum _{m=M}^N⦋m/j⦌A=\sum _{k=M-K}^{N-K}B$$
35	9 34	syl5eq	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M-K}^{N-K}B$$