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 15970

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 15966	. 2 ⊢ ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴
2		fveq2 6881	. . . 4 ⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
3		fprodser.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		eluzelz 12867	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6	5	zcnd 12703	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		eluzel2 12862	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
8	3, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	zcnd 12703	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10		1cnd 11235	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
11	6, 9, 10	subadd23d 11621	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀)))
12	11	eqcomd 2742	. . . . 5 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1))
13		uznn0sub 12896	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ₀)
14	3, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
15		nn0p1nn 12545	. . . . . 6 ⊢ ((𝑁 − 𝑀) ∈ ℕ₀ → ((𝑁 − 𝑀) + 1) ∈ ℕ)
16	14, 15	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ)
17	12, 16	eqeltrd 2835	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ)
18	10, 9	pncan3d 11602	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
19	6, 10, 9	pnpncand 11663	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁)
20	18, 19	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
21	20	eleq2d 2821	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁)))
22	21	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁))
23		elfzelz 13546	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ)
24	23	zcnd 12703	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ)
26		peano2zm 12640	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	8, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28	27	zcnd 12703	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
29	28	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ)
30	25, 29	npcand 11603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝)
31		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁))
32	30, 31	eqeltrd 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
33		ovex 7443	. . . . . . . . . 10 ⊢ (𝑝 − (𝑀 − 1)) ∈ V
34		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
35	34	eleq1d 2820	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)))
36	33, 35	sbcie 3812	. . . . . . . . 9 ⊢ ([(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
37	32, 36	sylibr 234	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
38	22, 37	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
39	38	ralrimiva 3133	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
40		1zzd 12628	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
41	17	nnzd 12620	. . . . . . 7 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ)
42		fzshftral 13637	. . . . . . 7 ⊢ ((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)))
43	40, 41, 27, 42	syl3anc 1373	. . . . . 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 13582	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑝 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
50	45, 46, 47, 48, 49	syl22anc 838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))))
51	31, 50	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))))
52	9, 10	nncand 11604	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1)
53	6, 9, 10	subsub2d 11628	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀)))
54	52, 53	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
55	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
56	51, 55	eleqtrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))))
57	30	eqcomd 2742	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
58	34	rspceeqv 3629	. . . . . . . 8 ⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
59	56, 57, 58	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
60		elfzelz 13546	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ)
61	60	zcnd 12703	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ)
62		elfzelz 13546	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ)
63	62	zcnd 12703	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ)
64	61, 63	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ))
65		eqtr2 2757	. . . . . . . . . . 11 ⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
66		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ)
67		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ)
68	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ)
69	66, 67, 68	addcan2d 11444	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)) ↔ 𝑛 = 𝑚))
70	65, 69	imbitrid 244	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
71	64, 70	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
72	71	ralrimivva 3188	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
73	72	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
74		oveq1 7417	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
75	74	eqeq2d 2747	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1))))
76	75	reu4 3719	. . . . . . 7 ⊢ (∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ↔ (∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)))
77	59, 73, 76	sylanbrc 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
78	77	ralrimiva 3133	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
79		eqid 2736	. . . . . 6 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))
80	79	f1ompt 7106	. . . . 5 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))))
81	44, 78, 80	sylanbrc 583	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁))
82		fprodser.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ)
83	82	fmpttd 7110	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ)
84	83	ffvelcdmda 7079	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ)
85		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))
86		1zzd 12628	. . . . . . . . 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 13580	. . . . . . . . 9 ⊢ (((1 ∈ ℤ ∧ (𝑁 + (1 − 𝑀)) ∈ ℤ) ∧ (𝑚 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))))
91	86, 87, 88, 89, 90	syl22anc 838	. . . . . . . 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 2837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁))
95		fprodser.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
96	95	ralrimiva 3133	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴)
97		nfcsb1v 3903	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
98	97	nfeq2 2917	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
99		fveq2 6881	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1))))
100		csbeq1a 3893	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
101	99, 100	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
102	98, 101	rspc 3594	. . . . . . 7 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴 → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
103	96, 102	mpan9 506	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
104	94, 103	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
105		f1of 6823	. . . . . . . 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 6983	. . . . . . 7 ⊢ (((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
108	106, 107	sylan 580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
109		ovex 7443	. . . . . . . . 9 ⊢ (𝑚 + (𝑀 − 1)) ∈ V
110	74, 79, 109	fvmpt 6991	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
111	110	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
112	111	fveq2d 6885	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1))))
113	108, 112	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1))))
114	111	fveq2d 6885	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))))
115	82	ralrimiva 3133	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
116	97	nfel1 2916	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ
117	100	eleq1d 2820	. . . . . . . . . 10 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
118	116, 117	rspc 3594	. . . . . . . . 9 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
119	115, 118	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
120	94, 119	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
121		eqid 2736	. . . . . . . 8 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)
122	121	fvmpts 6994	. . . . . . 7 ⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
123	94, 120, 122	syl2anc 584	. . . . . 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 15962	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))))
127		nnuz 12900	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
128	17, 127	eleqtrdi 2845	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ (ℤ_≥‘1))
129	128, 27, 113	seqshft2 14051	. . 3 ⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
130	18	seqeq1d 14030	. . . 4 ⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹))
131	130, 19	fveq12d 6888	. . 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 1540 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 ∃!wreu 3362 [wsbc 3770 ⦋csb 3879 ↦ cmpt 5206 ∘ ccom 5663 ⟶wf 6532 –1-1-onto→wf1o 6535 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 1c1 11135 + caddc 11137 · cmul 11139 − cmin 11471 ℕcn 12245 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ...cfz 13529 seqcseq 14024 ∏cprod 15924

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-oi 9529 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-z 12594 df-uz 12858 df-rp 13014 df-fz 13530 df-fzo 13677 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-prod 15925

This theorem is referenced by: fprodfac 15994 iprodclim3 16021

W3C validator