Theorem fsumrev2

Description: Reversal of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Hypotheses	fsumrev2.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fsumrev2.2	⊢ ( 𝑗 = ( ( 𝑀 + 𝑁 ) − 𝑘 ) → 𝐴 = 𝐵 )
Assertion	fsumrev2	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsumrev2.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
2		fsumrev2.2	⊢ ( 𝑗 = ( ( 𝑀 + 𝑁 ) − 𝑘 ) → 𝐴 = 𝐵 )
3		sum0	⊢ Σ 𝑗 ∈ ∅ 𝐴 = 0
4		sum0	⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
5	3 4	eqtr4i	⊢ Σ 𝑗 ∈ ∅ 𝐴 = Σ 𝑘 ∈ ∅ 𝐵
6		sumeq1	⊢ ( ( 𝑀 ... 𝑁 ) = ∅ → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑗 ∈ ∅ 𝐴 )
7		sumeq1	⊢ ( ( 𝑀 ... 𝑁 ) = ∅ → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
8	5 6 7	3eqtr4a	⊢ ( ( 𝑀 ... 𝑁 ) = ∅ → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )
9	8	adantl	⊢ ( ( 𝜑 ∧ ( 𝑀 ... 𝑁 ) = ∅ ) → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )
10		fzn0	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
11		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℤ )
13		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
15	12 14	zaddcld	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
16	1	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
17	15 12 14 16 2	fsumrev	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) 𝐵 )
18	12	zcnd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℂ )
19	14	zcnd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℂ )
20	18 19	pncand	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
21	18 19	pncan2d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑀 + 𝑁 ) − 𝑀 ) = 𝑁 )
22	20 21	oveq12d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) = ( 𝑀 ... 𝑁 ) )
23	22	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → Σ 𝑘 ∈ ( ( ( 𝑀 + 𝑁 ) − 𝑁 ) ... ( ( 𝑀 + 𝑁 ) − 𝑀 ) ) 𝐵 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )
24	17 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )
25	10 24	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝑀 ... 𝑁 ) ≠ ∅ ) → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )
26	9 25	pm2.61dane	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )