Theorem fsumshftd

Description: Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft . The proof demonstrates how this can be derived starting from from fsumshft . (Contributed by NM, 1-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fsumshftd.1	$$⊢\phi \to K\in \mathbb{Z}$$
2		fsumshftd.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		fsumshftd.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		fsumshftd.4	$$⊢\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ$$
5		fsumshftd.5	$$⊢\left(\phi \wedge j=k-K\right)\to A=B$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}wA$$
7		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋w/j⦌A$$
8		csbeq1a	$$⊢j=w\to A=⦋w/j⦌A$$
9	6 7 8	cbvsumi	$$⊢\sum _{j=M}^{N}A=\sum _{w=M}^N⦋w/j⦌A$$
10		nfv	$$⊢Ⅎj\left(\phi \wedge w\in \left(M\dots N\right)\right)$$
11	7	nfel1	$$⊢Ⅎj⦋w/j⦌A\in ℂ$$
12	10 11	nfim	$$⊢Ⅎj\left(\left(\phi \wedge w\in \left(M\dots N\right)\right)\to ⦋w/j⦌A\in ℂ\right)$$
13		eleq1w	$$⊢j=w\to \left(j\in \left(M\dots N\right)\leftrightarrow w\in \left(M\dots N\right)\right)$$
14	13	anbi2d	$$⊢j=w\to \left(\left(\phi \wedge j\in \left(M\dots N\right)\right)\leftrightarrow \left(\phi \wedge w\in \left(M\dots N\right)\right)\right)$$
15	8	eleq1d	$$⊢j=w\to \left(A\in ℂ\leftrightarrow ⦋w/j⦌A\in ℂ\right)$$
16	14 15	imbi12d	$$⊢j=w\to \left(\left(\left(\phi \wedge j\in \left(M\dots N\right)\right)\to A\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge w\in \left(M\dots N\right)\right)\to ⦋w/j⦌A\in ℂ\right)\right)$$
17	12 16 4	chvarfv	$$⊢\left(\phi \wedge w\in \left(M\dots N\right)\right)\to ⦋w/j⦌A\in ℂ$$
18		csbeq1	$$⊢w=k-K\to ⦋w/j⦌A=⦋\left(k-K\right)/j⦌A$$
19	1 2 3 17 18	fsumshft	$$⊢\phi \to \sum _{w=M}^N⦋w/j⦌A=\sum _{k=M+K}^{N+K}⦋\left(k-K\right)/j⦌A$$
20		ovexd	$$⊢\phi \to k-K\in \mathrm{V}$$
21	20 5	csbied	$$⊢\phi \to ⦋\left(k-K\right)/j⦌A=B$$
22	21	sumeq2sdv	$$⊢\phi \to \sum _{k=M+K}^{N+K}⦋\left(k-K\right)/j⦌A=\sum _{k=M+K}^{N+K}B$$
23	19 22	eqtrd	$$⊢\phi \to \sum _{w=M}^N⦋w/j⦌A=\sum _{k=M+K}^{N+K}B$$
24	9 23	eqtrid	$$⊢\phi \to \sum _{j=M}^{N}A=\sum _{k=M+K}^{N+K}B$$