Definition df-prod 15827

Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15610 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.)

Assertion

Ref	Expression
df-prod	⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥,𝑦   𝐴,𝑓,𝑚,𝑛,𝑥,𝑦   𝐵,𝑓,𝑚,𝑛,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Detailed syntax breakdown of Definition df-prod

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		vk	. . 3 setvar 𝑘
4	1, 2, 3	cprod 15826	. 2 class ∏𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1540	. . . . . . . 8 class 𝑚
7		cuz 12751	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6492	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3901	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vy	. . . . . . . . . . 11 setvar 𝑦
11	10	cv 1540	. . . . . . . . . 10 class 𝑦
12		cc0 11026	. . . . . . . . . 10 class 0
13	11, 12	wne 2932	. . . . . . . . 9 wff 𝑦 ≠ 0
14		cmul 11031	. . . . . . . . . . 11 class ·
15		cz 12488	. . . . . . . . . . . 12 class ℤ
16	3	cv 1540	. . . . . . . . . . . . . 14 class 𝑘
17	16, 1	wcel 2113	. . . . . . . . . . . . 13 wff 𝑘 ∈ 𝐴
18		c1 11027	. . . . . . . . . . . . 13 class 1
19	17, 2, 18	cif 4479	. . . . . . . . . . . 12 class if(𝑘 ∈ 𝐴, 𝐵, 1)
20	3, 15, 19	cmpt 5179	. . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
21		vn	. . . . . . . . . . . 12 setvar 𝑛
22	21	cv 1540	. . . . . . . . . . 11 class 𝑛
23	14, 20, 22	cseq 13924	. . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
24		cli 15407	. . . . . . . . . 10 class ⇝
25	23, 11, 24	wbr 5098	. . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦
26	13, 25	wa 395	. . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
27	26, 10	wex 1780	. . . . . . 7 wff ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
28	27, 21, 8	wrex 3060	. . . . . 6 wff ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
29	14, 20, 6	cseq 13924	. . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
30		vx	. . . . . . . 8 setvar 𝑥
31	30	cv 1540	. . . . . . 7 class 𝑥
32	29, 31, 24	wbr 5098	. . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥
33	9, 28, 32	w3a 1086	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
34	33, 5, 15	wrex 3060	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
35		cfz 13423	. . . . . . . . 9 class ...
36	18, 6, 35	co 7358	. . . . . . . 8 class (1...𝑚)
37		vf	. . . . . . . . 9 setvar 𝑓
38	37	cv 1540	. . . . . . . 8 class 𝑓
39	36, 1, 38	wf1o 6491	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
40		cn 12145	. . . . . . . . . . 11 class ℕ
41	22, 38	cfv 6492	. . . . . . . . . . . 12 class (𝑓‘𝑛)
42	3, 41, 2	csb 3849	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
43	21, 40, 42	cmpt 5179	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
44	14, 43, 18	cseq 13924	. . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
45	6, 44	cfv 6492	. . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
46	31, 45	wceq 1541	. . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
47	39, 46	wa 395	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
48	47, 37	wex 1780	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
49	48, 5, 40	wrex 3060	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
50	34, 49	wo 847	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
51	50, 30	cio 6446	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
52	4, 51	wceq 1541	1 wff ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  prodex  15828  prodeq1f  15829  prodeq1  15830  nfcprod1  15831  nfcprod  15832  prodeq2w  15833  prodeq2ii  15834  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  prodeq2sdv  15846  zprod  15860  fprod  15864  prodeq2si  36398  prodeq12sdv  36412  cbvprodvw2  36441  cbvproddavw  36474  cbvproddavw2  36490