fprodser - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fprodser		Structured version Visualization version GIF version

Theorem fprodser 15884

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.)

**Hypotheses**
Ref	Expression
fprodser.1	⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
fprodser.2	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
fprodser.3	⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)

**Assertion**
Ref	Expression
fprodser	⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁))

Distinct variable groups: 𝑘,𝐹 𝜑,𝑘 𝑘,𝑀 𝑘,𝑁 Allowed substitution hint: 𝐴(𝑘)

Proof of Theorem fprodser Dummy variables 𝑗 𝑚 𝑛 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prodfc 15880	. 2 ⊢ ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴
2		fveq2 6842	. . . 4 ⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
3		fprodser.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		eluzelz 12773	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6	5	zcnd 12609	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		eluzel2 12768	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
8	3, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	zcnd 12609	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10		1cnd 11139	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
11	6, 9, 10	subadd23d 11526	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀)))
12	11	eqcomd 2743	. . . . 5 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1))
13		uznn0sub 12798	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ₀)
14	3, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
15		nn0p1nn 12452	. . . . . 6 ⊢ ((𝑁 − 𝑀) ∈ ℕ₀ → ((𝑁 − 𝑀) + 1) ∈ ℕ)
16	14, 15	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ)
17	12, 16	eqeltrd 2837	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ)
18	10, 9	pncan3d 11507	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
19	6, 10, 9	pnpncand 11570	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁)
20	18, 19	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
21	20	eleq2d 2823	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁)))
22	21	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁))
23		elfzelz 13452	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ)
24	23	zcnd 12609	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ)
26		peano2zm 12546	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	8, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28	27	zcnd 12609	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
29	28	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ)
30	25, 29	npcand 11508	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝)
31		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁))
32	30, 31	eqeltrd 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
33		ovex 7401	. . . . . . . . . 10 ⊢ (𝑝 − (𝑀 − 1)) ∈ V
34		oveq1 7375	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
35	34	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)))
36	33, 35	sbcie 3784	. . . . . . . . 9 ⊢ ([(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
37	32, 36	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
38	22, 37	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
39	38	ralrimiva 3130	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
40		1zzd 12534	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
41	17	nnzd 12526	. . . . . . 7 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ)
42		fzshftral 13543	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)))
43	40, 41, 27, 42	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)))
44	39, 43	mpbird 257	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
45	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
46	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ)
47	23	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℤ)
48	27	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℤ)
49		fzsubel 13488	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑝 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
50	45, 46, 47, 48, 49	syl22anc 839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
51	31, 50	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))))
52	9, 10	nncand 11509	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1)
53	6, 9, 10	subsub2d 11533	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀)))
54	52, 53	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
55	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
56	51, 55	eleqtrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))))
57	30	eqcomd 2743	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
58	34	rspceeqv 3601	. . . . . . . 8 ⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
59	56, 57, 58	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
60		elfzelz 13452	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ)
61	60	zcnd 12609	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ)
62		elfzelz 13452	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ)
63	62	zcnd 12609	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ)
64	61, 63	anim12i 614	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ))
65		eqtr2 2758	. . . . . . . . . . 11 ⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
66		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ)
67		simprr 773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ)
68	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ)
69	66, 67, 68	addcan2d 11349	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)) ↔ 𝑛 = 𝑚))
70	65, 69	imbitrid 244	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
71	64, 70	sylan2 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
72	71	ralrimivva 3181	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
73	72	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
74		oveq1 7375	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
75	74	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1))))
76	75	reu4 3691	. . . . . . 7 ⊢ (∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ↔ (∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)))
77	59, 73, 76	sylanbrc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
78	77	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
79		eqid 2737	. . . . . 6 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))
80	79	f1ompt 7065	. . . . 5 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))))
81	44, 78, 80	sylanbrc 584	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁))
82		fprodser.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
83	82	fmpttd 7069	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ)
84	83	ffvelcdmda 7038	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ)
85		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))
86		1zzd 12534	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 1 ∈ ℤ)
87	41	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑁 + (1 − 𝑀)) ∈ ℤ)
88	62	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ ℤ)
89	27	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑀 − 1) ∈ ℤ)
90		fzaddel 13486	. . . . . . . . 9 ⊢ (((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))))
91	86, 87, 88, 89, 90	syl22anc 839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))))
92	85, 91	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
93	20	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
94	92, 93	eleqtrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁))
95		fprodser.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
96	95	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴)
97		nfcsb1v 3875	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
98	97	nfeq2 2917	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
99		fveq2 6842	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1))))
100		csbeq1a 3865	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
101	99, 100	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
102	98, 101	rspc 3566	. . . . . . 7 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴 → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
103	96, 102	mpan9 506	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
104	94, 103	syldan 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
105		f1of 6782	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁))
106	81, 105	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁))
107		fvco3 6941	. . . . . . 7 ⊢ (((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
108	106, 107	sylan 581	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
109		ovex 7401	. . . . . . . . 9 ⊢ (𝑚 + (𝑀 − 1)) ∈ V
110	74, 79, 109	fvmpt 6949	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
111	110	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
112	111	fveq2d 6846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1))))
113	108, 112	eqtrd 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1))))
114	111	fveq2d 6846	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))))
115	82	ralrimiva 3130	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
116	97	nfel1 2916	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ
117	100	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
118	116, 117	rspc 3566	. . . . . . . . 9 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
119	115, 118	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
120	94, 119	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
121		eqid 2737	. . . . . . . 8 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)
122	121	fvmpts 6953	. . . . . . 7 ⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
123	94, 120, 122	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
124	114, 123	eqtrd 2772	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
125	104, 113, 124	3eqtr4d 2782	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
126	2, 17, 81, 84, 125	fprod 15876	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))))
127		nnuz 12802	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
128	17, 127	eleqtrdi 2847	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ (ℤ_≥‘1))
129	128, 27, 113	seqshft2 13963	. . 3 ⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
130	18	seqeq1d 13942	. . . 4 ⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹))
131	130, 19	fveq12d 6849	. . 3 ⊢ (𝜑 → (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (seq𝑀( · , 𝐹)‘𝑁))
132	126, 129, 131	3eqtrd 2776	. 2 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq𝑀( · , 𝐹)‘𝑁))
133	1, 132	eqtr3id 2786	1 ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 ∃!wreu 3350 [wsbc 3742 ⦋csb 3851 ↦ cmpt 5181 ∘ ccom 5636 ⟶wf 6496 –1-1-onto→wf1o 6499 ‘cfv 6500 (class class class)co 7368 ℂcc 11036 1c1 11039 + caddc 11041 · cmul 11043 − cmin 11376 ℕcn 12157 ℕ₀cn0 12413 ℤcz 12500 ℤ_≥cuz 12763 ...cfz 13435 seqcseq 13936 ∏cprod 15838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-z 12501 df-uz 12764 df-rp 12918 df-fz 13436 df-fzo 13583 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-prod 15839

This theorem is referenced by: fprodfac 15908 iprodclim3 15935

W3C validator