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 15922

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 15918	. 2 ⊢ ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴
2		fveq2 6861	. . . 4 ⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
3		fprodser.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		eluzelz 12810	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
6	5	zcnd 12646	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
7		eluzel2 12805	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
8	3, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
9	8	zcnd 12646	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10		1cnd 11176	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
11	6, 9, 10	subadd23d 11562	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀)))
12	11	eqcomd 2736	. . . . 5 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1))
13		uznn0sub 12839	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 − 𝑀) ∈ ℕ₀)
14	3, 13	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℕ₀)
15		nn0p1nn 12488	. . . . . 6 ⊢ ((𝑁 − 𝑀) ∈ ℕ₀ → ((𝑁 − 𝑀) + 1) ∈ ℕ)
16	14, 15	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ)
17	12, 16	eqeltrd 2829	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ)
18	10, 9	pncan3d 11543	. . . . . . . . . . 11 ⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
19	6, 10, 9	pnpncand 11606	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁)
20	18, 19	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁))
21	20	eleq2d 2815	. . . . . . . . 9 ⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁)))
22	21	biimpa 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁))
23		elfzelz 13492	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ)
24	23	zcnd 12646	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ)
26		peano2zm 12583	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
27	8, 26	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
28	27	zcnd 12646	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℂ)
29	28	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ)
30	25, 29	npcand 11544	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝)
31		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁))
32	30, 31	eqeltrd 2829	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))
33		ovex 7423	. . . . . . . . . 10 ⊢ (𝑝 − (𝑀 − 1)) ∈ V
34		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
35	34	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)))
36	33, 35	sbcie 3798	. . . . . . . . 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 3126	. . . . . 6 ⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))
40		1zzd 12571	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
41	17	nnzd 12563	. . . . . . 7 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ)
42		fzshftral 13583	. . . . . . 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 13528	. . . . . . . . . . 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 11545	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1)
53	6, 9, 10	subsub2d 11569	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀)))
54	52, 53	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
55	54	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀))))
56	51, 55	eleqtrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))))
57	30	eqcomd 2736	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))
58	34	rspceeqv 3614	. . . . . . . 8 ⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
59	56, 57, 58	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
60		elfzelz 13492	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ)
61	60	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ)
62		elfzelz 13492	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ)
63	62	zcnd 12646	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ)
64	61, 63	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ))
65		eqtr2 2751	. . . . . . . . . . 11 ⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
66		simprl 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ)
67		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ)
68	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ)
69	66, 67, 68	addcan2d 11385	. . . . . . . . . . 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 3181	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
73	72	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))
74		oveq1 7397	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)))
75	74	eqeq2d 2741	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1))))
76	75	reu4 3705	. . . . . . 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 3126	. . . . 5 ⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))
79		eqid 2730	. . . . . 6 ⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))
80	79	f1ompt 7086	. . . . 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 7090	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ)
84	83	ffvelcdmda 7059	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ)
85		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))
86		1zzd 12571	. . . . . . . . 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 13526	. . . . . . . . 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 2831	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁))
95		fprodser.1	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴)
96	95	ralrimiva 3126	. . . . . . 7 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴)
97		nfcsb1v 3889	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
98	97	nfeq2 2910	. . . . . . . 8 ⊢ Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴
99		fveq2 6861	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1))))
100		csbeq1a 3879	. . . . . . . . 9 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
101	99, 100	eqeq12d 2746	. . . . . . . 8 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴))
102	98, 101	rspc 3579	. . . . . . 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 6803	. . . . . . . 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 6963	. . . . . . 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 7423	. . . . . . . . 9 ⊢ (𝑚 + (𝑀 − 1)) ∈ V
110	74, 79, 109	fvmpt 6971	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
111	110	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1)))
112	111	fveq2d 6865	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1))))
113	108, 112	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1))))
114	111	fveq2d 6865	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))))
115	82	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ)
116	97	nfel1 2909	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ
117	100	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
118	116, 117	rspc 3579	. . . . . . . . 9 ⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ))
119	115, 118	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
120	94, 119	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)
121		eqid 2730	. . . . . . . 8 ⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)
122	121	fvmpts 6974	. . . . . . 7 ⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
123	94, 120, 122	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
124	114, 123	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)
125	104, 113, 124	3eqtr4d 2775	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)))
126	2, 17, 81, 84, 125	fprod 15914	. . 3 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))))
127		nnuz 12843	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
128	17, 127	eleqtrdi 2839	. . . 4 ⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ (ℤ_≥‘1))
129	128, 27, 113	seqshft2 14000	. . 3 ⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))
130	18	seqeq1d 13979	. . . 4 ⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹))
131	130, 19	fveq12d 6868	. . 3 ⊢ (𝜑 → (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (seq𝑀( · , 𝐹)‘𝑁))
132	126, 129, 131	3eqtrd 2769	. 2 ⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq𝑀( · , 𝐹)‘𝑁))
133	1, 132	eqtr3id 2779	1 ⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3045 ∃wrex 3054 ∃!wreu 3354 [wsbc 3756 ⦋csb 3865 ↦ cmpt 5191 ∘ ccom 5645 ⟶wf 6510 –1-1-onto→wf1o 6513 ‘cfv 6514 (class class class)co 7390 ℂcc 11073 1c1 11076 + caddc 11078 · cmul 11080 − cmin 11412 ℕcn 12193 ℕ₀cn0 12449 ℤcz 12536 ℤ_≥cuz 12800 ...cfz 13475 seqcseq 13973 ∏cprod 15876

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-oi 9470 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-z 12537 df-uz 12801 df-rp 12959 df-fz 13476 df-fzo 13623 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-prod 15877

This theorem is referenced by: fprodfac 15946 iprodclim3 15973

W3C validator