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

Metamath Proof Explorer

Theorem fprodrev

Description: Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 fprodshft.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fprodshft.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fprodshft.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fprodshft.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fprodrev.5 ⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → 𝐴 = 𝐵 )
6 fzfid ⊢ ( 𝜑 → ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∈ Fin )
7 eqid ⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) = ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → 𝐾 ∈ ℤ )
9 elfzelz ⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → 𝑗 ∈ ℤ )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → 𝑗 ∈ ℤ )
11 8 10 zsubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( 𝐾 − 𝑗 ) ∈ ℤ )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
13 elfzelz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
15 12 14 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑘 ) ∈ ℤ )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
18 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑀 ∈ ℤ )
19 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑁 ∈ ℤ )
20 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝐾 ∈ ℤ )
21 9 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ℤ )
22 fzrev ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
23 18 19 20 21 22 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
24 17 23 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑗 ) ∈ ( 𝑀 ... 𝑁 ) )
25 16 24 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
26 oveq2 ⊢ ( 𝑘 = ( 𝐾 − 𝑗 ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
27 26 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
28 1 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝐾 ∈ ℂ )
30 9 zcnd ⊢ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → 𝑗 ∈ ℂ )
31 30 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 ∈ ℂ )
32 29 31 nncand ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
33 27 32 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
34 25 33 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) )
35 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 = ( 𝐾 − 𝑘 ) )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
37 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑀 ∈ ℤ )
38 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑁 ∈ ℤ )
39 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝐾 ∈ ℤ )
40 13 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ℤ )
41 fzrev2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
42 37 38 39 40 41 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) )
43 36 42 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
44 35 43 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
45 oveq2 ⊢ ( 𝑗 = ( 𝐾 − 𝑘 ) → ( 𝐾 − 𝑗 ) = ( 𝐾 − ( 𝐾 − 𝑘 ) ) )
46 45 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − 𝑗 ) = ( 𝐾 − ( 𝐾 − 𝑘 ) ) )
47 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝐾 ∈ ℂ )
48 13 zcnd ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℂ )
49 48 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 ∈ ℂ )
50 47 49 nncand ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝐾 − ( 𝐾 − 𝑘 ) ) = 𝑘 )
51 46 50 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → 𝑘 = ( 𝐾 − 𝑗 ) )
52 44 51 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) )
53 34 52 impbida ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ∧ 𝑘 = ( 𝐾 − 𝑗 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾 − 𝑘 ) ) ) )
54 7 11 15 53 f1od ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) : ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
55 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐾 − 𝑗 ) = ( 𝐾 − 𝑘 ) )
56 ovex ⊢ ( 𝐾 − 𝑘 ) ∈ V
57 55 7 56 fvmpt ⊢ ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( ( 𝑗 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↦ ( 𝐾 − 𝑗 ) ) ‘ 𝑘 ) = ( 𝐾 − 𝑘 ) )
59 5 6 54 58 4 fprodf1o ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) 𝐵 )