Definition df-prod 15839

Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15622 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 15838	. 2 class ∏𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1541	. . . . . . . 8 class 𝑚
7		cuz 12763	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6500	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3903	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vy	. . . . . . . . . . 11 setvar 𝑦
11	10	cv 1541	. . . . . . . . . 10 class 𝑦
12		cc0 11038	. . . . . . . . . 10 class 0
13	11, 12	wne 2933	. . . . . . . . 9 wff 𝑦 ≠ 0
14		cmul 11043	. . . . . . . . . . 11 class ·
15		cz 12500	. . . . . . . . . . . 12 class ℤ
16	3	cv 1541	. . . . . . . . . . . . . 14 class 𝑘
17	16, 1	wcel 2114	. . . . . . . . . . . . 13 wff 𝑘 ∈ 𝐴
18		c1 11039	. . . . . . . . . . . . 13 class 1
19	17, 2, 18	cif 4481	. . . . . . . . . . . 12 class if(𝑘 ∈ 𝐴, 𝐵, 1)
20	3, 15, 19	cmpt 5181	. . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
21		vn	. . . . . . . . . . . 12 setvar 𝑛
22	21	cv 1541	. . . . . . . . . . 11 class 𝑛
23	14, 20, 22	cseq 13936	. . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
24		cli 15419	. . . . . . . . . 10 class ⇝
25	23, 11, 24	wbr 5100	. . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦
26	13, 25	wa 395	. . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
27	26, 10	wex 1781	. . . . . . 7 wff ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
28	27, 21, 8	wrex 3062	. . . . . 6 wff ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
29	14, 20, 6	cseq 13936	. . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
30		vx	. . . . . . . 8 setvar 𝑥
31	30	cv 1541	. . . . . . 7 class 𝑥
32	29, 31, 24	wbr 5100	. . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥
33	9, 28, 32	w3a 1087	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
34	33, 5, 15	wrex 3062	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
35		cfz 13435	. . . . . . . . 9 class ...
36	18, 6, 35	co 7368	. . . . . . . 8 class (1...𝑚)
37		vf	. . . . . . . . 9 setvar 𝑓
38	37	cv 1541	. . . . . . . 8 class 𝑓
39	36, 1, 38	wf1o 6499	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
40		cn 12157	. . . . . . . . . . 11 class ℕ
41	22, 38	cfv 6500	. . . . . . . . . . . 12 class (𝑓‘𝑛)
42	3, 41, 2	csb 3851	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
43	21, 40, 42	cmpt 5181	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
44	14, 43, 18	cseq 13936	. . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
45	6, 44	cfv 6500	. . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
46	31, 45	wceq 1542	. . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
47	39, 46	wa 395	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
48	47, 37	wex 1781	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
49	48, 5, 40	wrex 3062	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
50	34, 49	wo 848	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
51	50, 30	cio 6454	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
52	4, 51	wceq 1542	1 wff ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  prodex  15840  prodeq1f  15841  prodeq1  15842  nfcprod1  15843  nfcprod  15844  prodeq2w  15845  prodeq2ii  15846  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  prodeq2sdv  15858  zprod  15872  fprod  15876  prodeq2si  36420  prodeq12sdv  36434  cbvprodvw2  36463  cbvproddavw  36496  cbvproddavw2  36512