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

Metamath Proof Explorer

Theorem fsumrev

Description: Reversal of a finite sum. (Contributed by NM, 26-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumrev.5 ⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → 𝐴 = 𝐵 )
Assertion fsumrev ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fsumrev.5 ⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → 𝐴 = 𝐵 )
6 fzfid ⊢ ( 𝜑 → ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∈ Fin )
7 eqid ⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) = ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) )
8 ovexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( 𝐾 − 𝑗 ) ∈ V )
9 ovexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑘 ) ∈ V )
10 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑀 ∈ ℤ )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑁 ∈ ℤ )
14 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝐾 ∈ ℤ )
15 11 elfzelzd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ℤ )
16 fzrev ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
17 12 13 14 15 16 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
18 11 17 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) )
19 10 18 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
20 10 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
21 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
22 zcn ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
23 nncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
24 21 22 23 syl2an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
25 1 15 24 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
26 20 25 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
27 19 26 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) )
28 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
29 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
30 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑀 ∈ ℤ )
31 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑁 ∈ ℤ )
32 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝐾 ∈ ℤ )
33 29 elfzelzd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ℤ )
34 fzrev2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
35 30 31 32 33 34 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
36 29 35 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
37 28 36 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
38 28 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑗 ) = ( 𝐾 − ( 𝐾 − 𝑘 ) ) )
39 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
40 nncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑘 ) ) = 𝑘 )
41 21 39 40 syl2an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝐾 − ( 𝐾 − 𝑘 ) ) = 𝑘 )
42 1 33 41 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑘 ) ) = 𝑘 )
43 38 42 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
44 37 43 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) )
45 27 44 impbida ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) )
46 7 8 9 45 f1od ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) : ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
47 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐾 − 𝑗 ) = ( 𝐾 − 𝑘 ) )
48 ovex ⊢ ( 𝐾 − 𝑘 ) ∈ V
49 47 7 48 fvmpt ⊢ ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
51 5 6 46 50 4 fsumf1o ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝐵 )