Definition df-prod 15925

Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15708 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 15924	. 2 class ∏𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . 9 setvar 𝑚
6	5	cv 1539	. . . . . . . 8 class 𝑚
7		cuz 12857	. . . . . . . 8 class ℤ≥
8	6, 7	cfv 6536	. . . . . . 7 class (ℤ≥‘𝑚)
9	1, 8	wss 3931	. . . . . 6 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vy	. . . . . . . . . . 11 setvar 𝑦
11	10	cv 1539	. . . . . . . . . 10 class 𝑦
12		cc0 11134	. . . . . . . . . 10 class 0
13	11, 12	wne 2933	. . . . . . . . 9 wff 𝑦 ≠ 0
14		cmul 11139	. . . . . . . . . . 11 class ·
15		cz 12593	. . . . . . . . . . . 12 class ℤ
16	3	cv 1539	. . . . . . . . . . . . . 14 class 𝑘
17	16, 1	wcel 2109	. . . . . . . . . . . . 13 wff 𝑘 ∈ 𝐴
18		c1 11135	. . . . . . . . . . . . 13 class 1
19	17, 2, 18	cif 4505	. . . . . . . . . . . 12 class if(𝑘 ∈ 𝐴, 𝐵, 1)
20	3, 15, 19	cmpt 5206	. . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
21		vn	. . . . . . . . . . . 12 setvar 𝑛
22	21	cv 1539	. . . . . . . . . . 11 class 𝑛
23	14, 20, 22	cseq 14024	. . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
24		cli 15505	. . . . . . . . . 10 class ⇝
25	23, 11, 24	wbr 5124	. . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦
26	13, 25	wa 395	. . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
27	26, 10	wex 1779	. . . . . . 7 wff ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
28	27, 21, 8	wrex 3061	. . . . . 6 wff ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
29	14, 20, 6	cseq 14024	. . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
30		vx	. . . . . . . 8 setvar 𝑥
31	30	cv 1539	. . . . . . 7 class 𝑥
32	29, 31, 24	wbr 5124	. . . . . 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 3061	. . . 4 wff ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
35		cfz 13529	. . . . . . . . 9 class ...
36	18, 6, 35	co 7410	. . . . . . . 8 class (1...𝑚)
37		vf	. . . . . . . . 9 setvar 𝑓
38	37	cv 1539	. . . . . . . 8 class 𝑓
39	36, 1, 38	wf1o 6535	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
40		cn 12245	. . . . . . . . . . 11 class ℕ
41	22, 38	cfv 6536	. . . . . . . . . . . 12 class (𝑓‘𝑛)
42	3, 41, 2	csb 3879	. . . . . . . . . . 11 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
43	21, 40, 42	cmpt 5206	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
44	14, 43, 18	cseq 14024	. . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))
45	6, 44	cfv 6536	. . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
46	31, 45	wceq 1540	. . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)
47	39, 46	wa 395	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
48	47, 37	wex 1779	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))
49	48, 5, 40	wrex 3061	. . . 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 6487	. 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
52	4, 51	wceq 1540	1 wff ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))

This definition is referenced by:  prodex  15926  prodeq1f  15927  prodeq1  15928  nfcprod1  15929  nfcprod  15930  prodeq2w  15931  prodeq2ii  15932  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  prodeq2sdv  15944  zprod  15958  fprod  15962  prodeq2si  36227  prodeq12sdv  36241  cbvprodvw2  36270  cbvproddavw  36303  cbvproddavw2  36319