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 syl5ib ( ( 𝜑 ∧ ( 𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( ( 𝑝 = ( 𝑛 + ( 𝑀 − 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 ffvelrnda ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ 𝐴 ) ‘ 𝑗 ) ∈ ℂ )
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 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )