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

Proof

Step	Hyp	Ref	Expression
1		fsumrev.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		fsumrev.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		fsumrev.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		fsumrev.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5		fsumshftm.5	⊢ ( 𝑗 = ( 𝑘 + 𝐾 ) → 𝐴 = 𝐵 )
6		nfcv	⊢ Ⅎ 𝑚 𝐴
7		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐴
8		csbeq1a	⊢ ( 𝑗 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑗 ⦌ 𝐴 )
9	6 7 8	cbvsumi	⊢ Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴
10	1	znegcld	⊢ ( 𝜑 → - 𝐾 ∈ ℤ )
11	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
12	7	nfel1	⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ
13	8	eleq1d	⊢ ( 𝑗 = 𝑚 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
14	12 13	rspc	⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
15	11 14	mpan9	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ )
16		csbeq1	⊢ ( 𝑚 = ( 𝑘 − - 𝐾 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
17	10 2 3 15 16	fsumshft	⊢ ( 𝜑 → Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
18	2	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
19	1	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
20	18 19	negsubd	⊢ ( 𝜑 → ( 𝑀 + - 𝐾 ) = ( 𝑀 − 𝐾 ) )
21	3	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
22	21 19	negsubd	⊢ ( 𝜑 → ( 𝑁 + - 𝐾 ) = ( 𝑁 − 𝐾 ) )
23	20 22	oveq12d	⊢ ( 𝜑 → ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) = ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) )
24	23	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
25		elfzelz	⊢ ( 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) → 𝑘 ∈ ℤ )
26	25	zcnd	⊢ ( 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) → 𝑘 ∈ ℂ )
27		subneg	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑘 − - 𝐾 ) = ( 𝑘 + 𝐾 ) )
28	26 19 27	syl2anr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ( 𝑘 − - 𝐾 ) = ( 𝑘 + 𝐾 ) )
29	28	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 + 𝐾 ) / 𝑗 ⦌ 𝐴 )
30		ovex	⊢ ( 𝑘 + 𝐾 ) ∈ V
31	30 5	csbie	⊢ ⦋ ( 𝑘 + 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵
32	29 31	syl6eq	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵 )
33	32	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )
34	17 24 33	3eqtrd	⊢ ( 𝜑 → Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )
35	9 34	syl5eq	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )