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 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )