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 15356

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 15352	. 2 ⊢ ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴
2		fveq2 6662	. . . 4 ⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
3		fprodser.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		eluzelz 12297	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6	5	zcnd 12132	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		eluzel2 12292	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
8	3, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	zcnd 12132	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10		1cnd 10679	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
11	6, 9, 10	subadd23d 11062	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀)))
12	11	eqcomd 2764	. . . . 5 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1))
13		uznn0sub 12322	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ₀)
14	3, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
15		nn0p1nn 11978	. . . . . 6 ⊢ ((𝑁 − 𝑀) ∈ ℕ₀ → ((𝑁 − 𝑀) + 1) ∈ ℕ)
16	14, 15	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ)
17	12, 16	eqeltrd 2852	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ)
18	10, 9	pncan3d 11043	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
19	6, 10, 9	pnpncand 11104	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁)
20	18, 19	oveq12d 7173	. . . . . . . . . 10 ⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
21	20	eleq2d 2837	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁)))
22	21	biimpa 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁))
23		elfzelz 12961	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ)
24	23	zcnd 12132	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ)
25	24	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ)
26		peano2zm 12069	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	8, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28	27	zcnd 12132	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
29	28	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ)
30	25, 29	npcand 11044	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝)
31		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁))
32	30, 31	eqeltrd 2852	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
33		ovex 7188	. . . . . . . . . 10 ⊢ (𝑝 − (𝑀 − 1)) ∈ V
34		oveq1 7162	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
35	34	eleq1d 2836	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)))
36	33, 35	sbcie 3739	. . . . . . . . 9 ⊢ ([(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
37	32, 36	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
38	22, 37	syldan 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
39	38	ralrimiva 3113	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
40		1zzd 12057	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
41	17	nnzd 12130	. . . . . . 7 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ)
42		fzshftral 13049	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)))
43	40, 41, 27, 42	syl3anc 1368	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)))
44	39, 43	mpbird 260	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
45	8	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
46	5	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ)
47	23	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℤ)
48	27	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℤ)
49		fzsubel 12997	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑝 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
50	45, 46, 47, 48, 49	syl22anc 837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
51	31, 50	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))))
52	9, 10	nncand 11045	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1)
53	6, 9, 10	subsub2d 11069	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀)))
54	52, 53	oveq12d 7173	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
55	54	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
56	51, 55	eleqtrd 2854	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))))
57	30	eqcomd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
58	34	rspceeqv 3558	. . . . . . . 8 ⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
59	56, 57, 58	syl2anc 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
60		elfzelz 12961	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ)
61	60	zcnd 12132	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ)
62		elfzelz 12961	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ)
63	62	zcnd 12132	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ)
64	61, 63	anim12i 615	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ))
65		eqtr2 2779	. . . . . . . . . . 11 ⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
66		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ)
67		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ)
68	28	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ)
69	66, 67, 68	addcan2d 10887	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)) ↔ 𝑛 = 𝑚))
70	65, 69	syl5ib 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
71	64, 70	sylan2 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
72	71	ralrimivva 3120	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
73	72	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
74		oveq1 7162	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
75	74	eqeq2d 2769	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1))))
76	75	reu4 3647	. . . . . . 7 ⊢ (∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ↔ (∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)))
77	59, 73, 76	sylanbrc 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
78	77	ralrimiva 3113	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
79		eqid 2758	. . . . . 6 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))
80	79	f1ompt 6871	. . . . 5 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))))
81	44, 78, 80	sylanbrc 586	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁))
82		fprodser.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
83	82	fmpttd 6875	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ)
84	83	ffvelrnda 6847	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ)
85		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))
86		1zzd 12057	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 1 ∈ ℤ)
87	41	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑁 + (1 − 𝑀)) ∈ ℤ)
88	62	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ ℤ)
89	27	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑀 − 1) ∈ ℤ)
90		fzaddel 12995	. . . . . . . . 9 ⊢ (((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))))
91	86, 87, 88, 89, 90	syl22anc 837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))))
92	85, 91	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
93	20	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
94	92, 93	eleqtrd 2854	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁))
95		fprodser.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
96	95	ralrimiva 3113	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴)
97		nfcsb1v 3831	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
98	97	nfeq2 2936	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
99		fveq2 6662	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1))))
100		csbeq1a 3821	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
101	99, 100	eqeq12d 2774	. . . . . . . 8 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
102	98, 101	rspc 3531	. . . . . . 7 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴 → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
103	96, 102	mpan9 510	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
104	94, 103	syldan 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
105		f1of 6606	. . . . . . . 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 6755	. . . . . . 7 ⊢ (((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
108	106, 107	sylan 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
109		ovex 7188	. . . . . . . . 9 ⊢ (𝑚 + (𝑀 − 1)) ∈ V
110	74, 79, 109	fvmpt 6763	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
111	110	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
112	111	fveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1))))
113	108, 112	eqtrd 2793	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1))))
114	111	fveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))))
115	82	ralrimiva 3113	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
116	97	nfel1 2935	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ
117	100	eleq1d 2836	. . . . . . . . . 10 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
118	116, 117	rspc 3531	. . . . . . . . 9 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
119	115, 118	mpan9 510	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
120	94, 119	syldan 594	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
121		eqid 2758	. . . . . . . 8 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)
122	121	fvmpts 6766	. . . . . . 7 ⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
123	94, 120, 122	syl2anc 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
124	114, 123	eqtrd 2793	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
125	104, 113, 124	3eqtr4d 2803	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
126	2, 17, 81, 84, 125	fprod 15348	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))))
127		nnuz 12326	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
128	17, 127	eleqtrdi 2862	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ (ℤ_≥‘1))
129	128, 27, 113	seqshft2 13451	. . 3 ⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
130	18	seqeq1d 13429	. . . 4 ⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹))
131	130, 19	fveq12d 6669	. . 3 ⊢ (𝜑 → (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (seq𝑀( · , 𝐹)‘𝑁))
132	126, 129, 131	3eqtrd 2797	. 2 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq𝑀( · , 𝐹)‘𝑁))
133	1, 132	syl5eqr 2807	1 ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3070 ∃wrex 3071 ∃!wreu 3072 [wsbc 3698 ⦋csb 3807 ↦ cmpt 5115 ∘ ccom 5531 ⟶wf 6335 –1-1-onto→wf1o 6338 ‘cfv 6339 (class class class)co 7155 ℂcc 10578 1c1 10581 + caddc 10583 · cmul 10585 − cmin 10913 ℕcn 11679 ℕ₀cn0 11939 ℤcz 12025 ℤ_≥cuz 12287 ...cfz 12944 seqcseq 13423 ∏cprod 15312

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5159 ax-sep 5172 ax-nul 5179 ax-pow 5237 ax-pr 5301 ax-un 7464 ax-inf2 9142 ax-cnex 10636 ax-resscn 10637 ax-1cn 10638 ax-icn 10639 ax-addcl 10640 ax-addrcl 10641 ax-mulcl 10642 ax-mulrcl 10643 ax-mulcom 10644 ax-addass 10645 ax-mulass 10646 ax-distr 10647 ax-i2m1 10648 ax-1ne0 10649 ax-1rid 10650 ax-rnegex 10651 ax-rrecex 10652 ax-cnre 10653 ax-pre-lttri 10654 ax-pre-lttrn 10655 ax-pre-ltadd 10656 ax-pre-mulgt0 10657 ax-pre-sup 10658

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5036 df-opab 5098 df-mpt 5116 df-tr 5142 df-id 5433 df-eprel 5438 df-po 5446 df-so 5447 df-fr 5486 df-se 5487 df-we 5488 df-xp 5533 df-rel 5534 df-cnv 5535 df-co 5536 df-dm 5537 df-rn 5538 df-res 5539 df-ima 5540 df-pred 6130 df-ord 6176 df-on 6177 df-lim 6178 df-suc 6179 df-iota 6298 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-om 7585 df-1st 7698 df-2nd 7699 df-wrecs 7962 df-recs 8023 df-rdg 8061 df-1o 8117 df-er 8304 df-en 8533 df-dom 8534 df-sdom 8535 df-fin 8536 df-sup 8944 df-oi 9012 df-card 9406 df-pnf 10720 df-mnf 10721 df-xr 10722 df-ltxr 10723 df-le 10724 df-sub 10915 df-neg 10916 df-div 11341 df-nn 11680 df-2 11742 df-3 11743 df-n0 11940 df-z 12026 df-uz 12288 df-rp 12436 df-fz 12945 df-fzo 13088 df-seq 13424 df-exp 13485 df-hash 13746 df-cj 14511 df-re 14512 df-im 14513 df-sqrt 14647 df-abs 14648 df-clim 14898 df-prod 15313

This theorem is referenced by: fprodfac 15380 iprodclim3 15407

W3C validator