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

Metamath Proof Explorer

Theorem fprodser

Description: A finite product expressed in terms of a partial product of an infinite sequence. The recursive definition of a finite product follows from here. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodser.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
fprodser.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fprodser.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
Assertion fprodser ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fprodser.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
2 fprodser.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 fprodser.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
4 prodfc ⊢ ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴
5 fveq2 ⊢ ( 𝑗 = ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) )
6 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
7 2 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8 7 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
9 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
10 2 9 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
11 10 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
12 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
13 8 11 12 subadd23d ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 1 ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
14 13 eqcomd ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑀 ) ) = ( ( 𝑁 − 𝑀 ) + 1 ) )
15 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
16 2 15 syl ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
17 nn0p1nn ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ0 → ( ( 𝑁 − 𝑀 ) + 1 ) ∈ ℕ )
18 16 17 syl ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) + 1 ) ∈ ℕ )
19 14 18 eqeltrd ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ℕ )
20 12 11 pncan3d ⊢ ( 𝜑 → ( 1 + ( 𝑀 − 1 ) ) = 𝑀 )
21 8 12 11 pnpncand ⊢ ( 𝜑 → ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) = 𝑁 )
22 20 21 oveq12d ⊢ ( 𝜑 → ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) = ( 𝑀 ... 𝑁 ) )
23 22 eleq2d ⊢ ( 𝜑 → ( 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) ↔ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) )
24 23 biimpa ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) ) → 𝑝 ∈ ( 𝑀 ... 𝑁 ) )
25 elfzelz ⊢ ( 𝑝 ∈ ( 𝑀 ... 𝑁 ) → 𝑝 ∈ ℤ )
26 25 zcnd ⊢ ( 𝑝 ∈ ( 𝑀 ... 𝑁 ) → 𝑝 ∈ ℂ )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑝 ∈ ℂ )
28 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
29 10 28 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
30 29 zcnd ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℂ )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ℂ )
32 27 31 npcand ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) = 𝑝 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑝 ∈ ( 𝑀 ... 𝑁 ) )
34 32 33 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
35 ovex ⊢ ( 𝑝 − ( 𝑀 − 1 ) ) ∈ V
36 oveq1 ⊢ ( 𝑛 = ( 𝑝 − ( 𝑀 − 1 ) ) → ( 𝑛 + ( 𝑀 − 1 ) ) = ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) )
37 36 eleq1d ⊢ ( 𝑛 = ( 𝑝 − ( 𝑀 − 1 ) ) → ( ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
38 35 37 sbcie ⊢ ( [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
39 34 38 sylibr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
40 24 39 syldan ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) ) → [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
42 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
43 19 nnzd ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ℤ )
44 fzshftral ⊢ ( ( 1 ∈ ℤ ∧ ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ↔ ∀ 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
45 42 43 29 44 syl3anc ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ↔ ∀ 𝑝 ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) [ ( 𝑝 − ( 𝑀 − 1 ) ) / 𝑛 ] ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
46 41 45 mpbird ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
47 10 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
48 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
49 25 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑝 ∈ ℤ )
50 29 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ℤ )
51 fzsubel ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑝 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) ) → ( 𝑝 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑝 − ( 𝑀 − 1 ) ) ∈ ( ( 𝑀 − ( 𝑀 − 1 ) ) ... ( 𝑁 − ( 𝑀 − 1 ) ) ) ) )
52 47 48 49 50 51 syl22anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑝 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑝 − ( 𝑀 − 1 ) ) ∈ ( ( 𝑀 − ( 𝑀 − 1 ) ) ... ( 𝑁 − ( 𝑀 − 1 ) ) ) ) )
53 33 52 mpbid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑝 − ( 𝑀 − 1 ) ) ∈ ( ( 𝑀 − ( 𝑀 − 1 ) ) ... ( 𝑁 − ( 𝑀 − 1 ) ) ) )
54 11 12 nncand ⊢ ( 𝜑 → ( 𝑀 − ( 𝑀 − 1 ) ) = 1 )
55 8 11 12 subsub2d ⊢ ( 𝜑 → ( 𝑁 − ( 𝑀 − 1 ) ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
56 54 55 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 − ( 𝑀 − 1 ) ) ... ( 𝑁 − ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑀 − ( 𝑀 − 1 ) ) ... ( 𝑁 − ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
58 53 57 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑝 − ( 𝑀 − 1 ) ) ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
59 32 eqcomd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑝 = ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) )
60 36 rspceeqv ⊢ ( ( ( 𝑝 − ( 𝑀 − 1 ) ) ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∧ 𝑝 = ( ( 𝑝 − ( 𝑀 − 1 ) ) + ( 𝑀 − 1 ) ) ) → ∃ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) )
61 58 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ∃ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) )
62 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) → 𝑛 ∈ ℤ )
63 62 zcnd ⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) → 𝑛 ∈ ℂ )
64 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) → 𝑚 ∈ ℤ )
65 64 zcnd ⊢ ( 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) → 𝑚 ∈ ℂ )
66 63 65 anim12i ⊢ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) )
67 eqtr2 ⊢ ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → ( 𝑛 + ( 𝑀 − 1 ) ) = ( 𝑚 + ( 𝑀 − 1 ) ) )
68 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → 𝑛 ∈ ℂ )
69 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → 𝑚 ∈ ℂ )
70 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝑀 − 1 ) ∈ ℂ )
71 68 69 70 addcan2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( ( 𝑛 + ( 𝑀 − 1 ) ) = ( 𝑚 + ( 𝑀 − 1 ) ) ↔ 𝑛 = 𝑚 ) )
72 67 71 imbitrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → 𝑛 = 𝑚 ) )
73 66 72 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) ) → ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → 𝑛 = 𝑚 ) )
74 73 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∀ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → 𝑛 = 𝑚 ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∀ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → 𝑛 = 𝑚 ) )
76 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 + ( 𝑀 − 1 ) ) = ( 𝑚 + ( 𝑀 − 1 ) ) )
77 76 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ↔ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) )
78 77 reu4 ⊢ ( ∃! 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ↔ ( ∃ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ∀ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ∧ 𝑝 = ( 𝑚 + ( 𝑀 − 1 ) ) ) → 𝑛 = 𝑚 ) ) )
79 61 75 78 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ) → ∃! 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) )
80 79 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ∃! 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) )
81 eqid ⊢ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) = ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) )
82 81 f1ompt ⊢ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ↔ ( ∀ 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ( 𝑛 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( 𝑀 ... 𝑁 ) ∃! 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) 𝑝 = ( 𝑛 + ( 𝑀 − 1 ) ) ) )
83 46 80 82 sylanbrc ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
84 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) : ( 𝑀 ... 𝑁 ) ⟶ ℂ )
85 84 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℂ )
86 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
87 1zzd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → 1 ∈ ℤ )
88 43 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ℤ )
89 64 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → 𝑚 ∈ ℤ )
90 29 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑀 − 1 ) ∈ ℤ )
91 fzaddel ⊢ ( ( ( 1 ∈ ℤ ∧ ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ℤ ) ∧ ( 𝑚 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) ) → ( 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↔ ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) ) )
92 87 88 89 90 91 syl22anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↔ ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) ) )
93 86 92 mpbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) )
94 22 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 1 + ( 𝑀 − 1 ) ) ... ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) = ( 𝑀 ... 𝑁 ) )
95 93 94 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) )
96 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 )
97 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴
98 97 nfeq2 ⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴
99 fveq2 ⊢ ( 𝑘 = ( 𝑚 + ( 𝑀 − 1 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) )
100 csbeq1a ⊢ ( 𝑘 = ( 𝑚 + ( 𝑀 − 1 ) ) → 𝐴 = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
101 99 100 eqeq12d ⊢ ( 𝑘 = ( 𝑚 + ( 𝑀 − 1 ) ) → ( ( 𝐹 ‘ 𝑘 ) = 𝐴 ↔ ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ) )
102 98 101 rspc ⊢ ( ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = 𝐴 → ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ) )
103 96 102 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
104 95 103 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
105 f1of ⊢ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) → ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ⟶ ( 𝑀 ... 𝑁 ) )
106 83 105 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ⟶ ( 𝑀 ... 𝑁 ) )
107 fvco3 ⊢ ( ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) : ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ⟶ ( 𝑀 ... 𝑁 ) ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) )
108 106 107 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) )
109 ovex ⊢ ( 𝑚 + ( 𝑀 − 1 ) ) ∈ V
110 76 81 109 fvmpt ⊢ ( 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) = ( 𝑚 + ( 𝑀 − 1 ) ) )
111 110 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) = ( 𝑚 + ( 𝑀 − 1 ) ) )
112 111 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) = ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) )
113 108 112 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) )
114 111 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) )
115 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
116 97 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ
117 100 eleq1d ⊢ ( 𝑘 = ( 𝑚 + ( 𝑀 − 1 ) ) → ( 𝐴 ∈ ℂ ↔ ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
118 116 117 rspc ⊢ ( ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ → ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) )
119 115 118 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ )
120 95 119 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ )
121 eqid ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 )
122 121 fvmpts ⊢ ( ( ( 𝑚 + ( 𝑀 − 1 ) ) ∈ ( 𝑀 ... 𝑁 ) ∧ ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 ∈ ℂ ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
123 95 120 122 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( 𝑚 + ( 𝑀 − 1 ) ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
124 114 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) = ⦋ ( 𝑚 + ( 𝑀 − 1 ) ) / 𝑘 ⦌ 𝐴 )
125 104 113 124 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ) → ( ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ ( ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ‘ 𝑚 ) ) )
126 5 19 83 85 125 fprod ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) = ( seq 1 ( · , ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ) ‘ ( 𝑁 + ( 1 − 𝑀 ) ) ) )
127 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
128 19 127 eleqtrdi ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑀 ) ) ∈ ( ℤ≥ ‘ 1 ) )
129 128 29 113 seqshft2 ⊢ ( 𝜑 → ( seq 1 ( · , ( 𝐹 ∘ ( 𝑛 ∈ ( 1 ... ( 𝑁 + ( 1 − 𝑀 ) ) ) ↦ ( 𝑛 + ( 𝑀 − 1 ) ) ) ) ) ‘ ( 𝑁 + ( 1 − 𝑀 ) ) ) = ( seq ( 1 + ( 𝑀 − 1 ) ) ( · , 𝐹 ) ‘ ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) )
130 20 seqeq1d ⊢ ( 𝜑 → seq ( 1 + ( 𝑀 − 1 ) ) ( · , 𝐹 ) = seq 𝑀 ( · , 𝐹 ) )
131 130 21 fveq12d ⊢ ( 𝜑 → ( seq ( 1 + ( 𝑀 − 1 ) ) ( · , 𝐹 ) ‘ ( ( 𝑁 + ( 1 − 𝑀 ) ) + ( 𝑀 − 1 ) ) ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )
132 126 129 131 3eqtrd ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )
133 4 132 eqtr3id ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )