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 15914

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 15910	. 2 ⊢ ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴
2		fveq2 6840	. . . 4 ⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
3		fprodser.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		eluzelz 12798	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6	5	zcnd 12634	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		eluzel2 12793	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
8	3, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	zcnd 12634	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10		1cnd 11139	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
11	6, 9, 10	subadd23d 11527	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀)))
12	11	eqcomd 2742	. . . . 5 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1))
13		uznn0sub 12823	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ₀)
14	3, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
15		nn0p1nn 12476	. . . . . 6 ⊢ ((𝑁 − 𝑀) ∈ ℕ₀ → ((𝑁 − 𝑀) + 1) ∈ ℕ)
16	14, 15	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ)
17	12, 16	eqeltrd 2836	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ)
18	10, 9	pncan3d 11508	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
19	6, 10, 9	pnpncand 11571	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁)
20	18, 19	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
21	20	eleq2d 2822	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁)))
22	21	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁))
23		elfzelz 13478	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ)
24	23	zcnd 12634	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ)
26		peano2zm 12570	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	8, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28	27	zcnd 12634	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
29	28	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ)
30	25, 29	npcand 11509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝)
31		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁))
32	30, 31	eqeltrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
33		ovex 7400	. . . . . . . . . 10 ⊢ (𝑝 − (𝑀 − 1)) ∈ V
34		oveq1 7374	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
35	34	eleq1d 2821	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)))
36	33, 35	sbcie 3770	. . . . . . . . 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 3129	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
40		1zzd 12558	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
41	17	nnzd 12550	. . . . . . 7 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ)
42		fzshftral 13569	. . . . . . 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 13514	. . . . . . . . . . 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 11510	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1)
53	6, 9, 10	subsub2d 11534	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀)))
54	52, 53	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
55	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
56	51, 55	eleqtrd 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))))
57	30	eqcomd 2742	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
58	34	rspceeqv 3587	. . . . . . . 8 ⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
59	56, 57, 58	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
60		elfzelz 13478	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ)
61	60	zcnd 12634	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ)
62		elfzelz 13478	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ)
63	62	zcnd 12634	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ)
64	61, 63	anim12i 614	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ))
65		eqtr2 2757	. . . . . . . . . . 11 ⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
66		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ)
67		simprr 773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ)
68	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ)
69	66, 67, 68	addcan2d 11350	. . . . . . . . . . 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 3180	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
73	72	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
74		oveq1 7374	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
75	74	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1))))
76	75	reu4 3677	. . . . . . 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 3129	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
79		eqid 2736	. . . . . 6 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))
80	79	f1ompt 7063	. . . . 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 7067	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ)
84	83	ffvelcdmda 7036	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ)
85		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))
86		1zzd 12558	. . . . . . . . 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 13512	. . . . . . . . 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 2838	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁))
95		fprodser.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
96	95	ralrimiva 3129	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴)
97		nfcsb1v 3861	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
98	97	nfeq2 2916	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
99		fveq2 6840	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1))))
100		csbeq1a 3851	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
101	99, 100	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
102	98, 101	rspc 3552	. . . . . . 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 6780	. . . . . . . 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 6939	. . . . . . 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 7400	. . . . . . . . 9 ⊢ (𝑚 + (𝑀 − 1)) ∈ V
110	74, 79, 109	fvmpt 6947	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
111	110	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
112	111	fveq2d 6844	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1))))
113	108, 112	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1))))
114	111	fveq2d 6844	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))))
115	82	ralrimiva 3129	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
116	97	nfel1 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ
117	100	eleq1d 2821	. . . . . . . . . 10 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
118	116, 117	rspc 3552	. . . . . . . . 9 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
119	115, 118	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
120	94, 119	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
121		eqid 2736	. . . . . . . 8 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)
122	121	fvmpts 6951	. . . . . . 7 ⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
123	94, 120, 122	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
124	114, 123	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
125	104, 113, 124	3eqtr4d 2781	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
126	2, 17, 81, 84, 125	fprod 15906	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))))
127		nnuz 12827	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
128	17, 127	eleqtrdi 2846	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ (ℤ_≥‘1))
129	128, 27, 113	seqshft2 13990	. . 3 ⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
130	18	seqeq1d 13969	. . . 4 ⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹))
131	130, 19	fveq12d 6847	. . 3 ⊢ (𝜑 → (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (seq𝑀( · , 𝐹)‘𝑁))
132	126, 129, 131	3eqtrd 2775	. 2 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq𝑀( · , 𝐹)‘𝑁))
133	1, 132	eqtr3id 2785	1 ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3051 ∃wrex 3061 ∃!wreu 3340 [wsbc 3728 ⦋csb 3837 ↦ cmpt 5166 ∘ ccom 5635 ⟶wf 6494 –1-1-onto→wf1o 6497 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 1c1 11039 + caddc 11041 · cmul 11043 − cmin 11377 ℕcn 12174 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 ...cfz 13461 seqcseq 13963 ∏cprod 15868

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 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-sup 9355 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-rp 12943 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-prod 15869

This theorem is referenced by: fprodfac 15938 iprodclim3 15965

W3C validator