Definition df-prod 15860

Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15640 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 15859	. 2 class ∏𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1546	. . . . . . . 8 class 𝑚
7		cuz 12779	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6485	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3883	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vy	. . . . . . . . . . 11 setvar 𝑦
11	10	cv 1546	. . . . . . . . . 10 class 𝑦
12		cc0 11029	. . . . . . . . . 10 class 0
13	11, 12	wne 2934	. . . . . . . . 9 wff 𝑦 ≠ 0
14		cmul 11034	. . . . . . . . . . 11 class ·
15		cz 12515	. . . . . . . . . . . 12 class ℤ
16	3	cv 1546	. . . . . . . . . . . . . 14 class 𝑘
17	16, 1	wcel 2119	. . . . . . . . . . . . 13 wff 𝑘 ∈ 𝐴
18		c1 11030	. . . . . . . . . . . . 13 class 1
19	17, 2, 18	cif 4454	. . . . . . . . . . . 12 class if(𝑘 ∈ 𝐴, 𝐵, 1)
20	3, 15, 19	cmpt 5153	. . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
21		vn	. . . . . . . . . . . 12 setvar 𝑛
22	21	cv 1546	. . . . . . . . . . 11 class 𝑛
23	14, 20, 22	cseq 13954	. . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
24		cli 15437	. . . . . . . . . 10 class ⇝
25	23, 11, 24	wbr 5072	. . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦
26	13, 25	wa 396	. . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
27	26, 10	wex 1786	. . . . . . 7 wff ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
28	27, 21, 8	wrex 3063	. . . . . 6 wff ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
29	14, 20, 6	cseq 13954	. . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
30		vx	. . . . . . . 8 setvar 𝑥
31	30	cv 1546	. . . . . . 7 class 𝑥
32	29, 31, 24	wbr 5072	. . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥
33	9, 28, 32	w3a 1092	. . . . 5 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
34	33, 5, 15	wrex 3063	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
35		cfz 13452	. . . . . . . . 9 class ...
36	18, 6, 35	co 7356	. . . . . . . 8 class (1...𝑚)
37		vf	. . . . . . . . 9 setvar 𝑓
38	37	cv 1546	. . . . . . . 8 class 𝑓
39	36, 1, 38	wf1o 6484	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
40		cn 12165	. . . . . . . . . . 11 class ℕ
41	22, 38	cfv 6485	. . . . . . . . . . . 12 class (𝑓‘𝑛)
42	3, 41, 2	csb 3831	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
43	21, 40, 42	cmpt 5153	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
44	14, 43, 18	cseq 13954	. . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
45	6, 44	cfv 6485	. . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
46	31, 45	wceq 1547	. . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
47	39, 46	wa 396	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
48	47, 37	wex 1786	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
49	48, 5, 40	wrex 3063	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
50	34, 49	wo 853	. . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
51	50, 30	cio 6439	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
52	4, 51	wceq 1547	1 wff ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  prodex  15861  prodeq1f  15862  prodeq1  15863  nfcprod1  15864  nfcprod  15865  prodeq2w  15866  prodeq2ii  15867  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  prodeq2sdv  15879  zprod  15893  fprod  15897  prodeq2si  36432  prodeq12sdv  36446  cbvprodvw2  36475  cbvproddavw  36508  cbvproddavw2  36524