This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐵 )