Theorem fsumshft

Description: Index shift of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014) (Proof shortened by AV, 8-Sep-2019)

	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 ℂ$$
	fsumshft.5	$$⊢j=k-K\to A=B$$
Assertion	fsumshft	$$⊢\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		fsumshft.5	$$⊢j=k-K\to A=B$$
6		fzfid	$$⊢\phi \to \left(M+K\dots N+K\right)\in \mathrm{Fin}$$
7	1 2 3	mptfzshft	$$⊢\phi \to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right):\left(M+K\dots N+K\right)\underset{1-1\; onto}{⟶}\left(M\dots N\right)$$
8		oveq1	$$⊢j=k\to j-K=k-K$$
9		eqid	$$⊢\left(j\in \left(M+K\dots N+K\right)⟼j-K\right)=\left(j\in \left(M+K\dots N+K\right)⟼j-K\right)$$
10		ovex	$$⊢k-K\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢k\in \left(M+K\dots N+K\right)\to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right)\left(k\right)=k-K$$
12	11	adantl	$$⊢\left(\phi \wedge k\in \left(M+K\dots N+K\right)\right)\to \left(j\in \left(M+K\dots N+K\right)⟼j-K\right)\left(k\right)=k-K$$
13	5 6 7 12 4	fsumf1o	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M+K}^{N+K}B$$