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	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	fsumshftd.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fsumshftd.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fsumshftd.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fsumshftd.5	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑘 − 𝐾 ) ) → 𝐴 = 𝐵 )
Assertion	fsumshftd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsumshftd.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		fsumshftd.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		fsumshftd.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		fsumshftd.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5		fsumshftd.5	⊢ ( ( 𝜑 ∧ 𝑗 = ( 𝑘 − 𝐾 ) ) → 𝐴 = 𝐵 )
6		nfcv	⊢ Ⅎ 𝑤 𝐴
7		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝐴
8		csbeq1a	⊢ ( 𝑗 = 𝑤 → 𝐴 = ⦋ 𝑤 / 𝑗 ⦌ 𝐴 )
9	6 7 8	cbvsumi	⊢ Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴
10		nfv	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) )
11	7	nfel1	⊢ Ⅎ 𝑗 ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ
12	10 11	nfim	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ )
13		eleq1w	⊢ ( 𝑗 = 𝑤 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) )
14	13	anbi2d	⊢ ( 𝑗 = 𝑤 → ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) ) )
15	8	eleq1d	⊢ ( 𝑗 = 𝑤 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
16	14 15	imbi12d	⊢ ( 𝑗 = 𝑤 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ ) ) )
17	12 16 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 ∈ ℂ )
18		csbeq1	⊢ ( 𝑤 = ( 𝑘 − 𝐾 ) → ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 )
19	1 2 3 17 18	fsumshft	⊢ ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 )
20		ovexd	⊢ ( 𝜑 → ( 𝑘 − 𝐾 ) ∈ V )
21	20 5	csbied	⊢ ( 𝜑 → ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵 )
22	21	sumeq2sdv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ⦋ ( 𝑘 − 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
23	19 22	eqtrd	⊢ ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑤 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
24	9 23	syl5eq	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )