Definition df-proddc 11577

Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sumdc 11380 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.) (Revised by Jim Kingdon, 21-Mar-2024.)

Assertion

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

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

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

Detailed syntax breakdown of Definition df-proddc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		vk	. . 3 setvar 𝑘
4	1, 2, 3	cprod 11576	. 2 class ∏𝑘 ∈ 𝐴 𝐵
5		vm	. . . . . . . . . 10 setvar 𝑚
6	5	cv 1363	. . . . . . . . 9 class 𝑚
7		cuz 9546	. . . . . . . . 9 class ℤ≥
8	6, 7	cfv 5231	. . . . . . . 8 class (ℤ≥‘𝑚)
9	1, 8	wss 3144	. . . . . . 7 wff 𝐴 ⊆ (ℤ≥‘𝑚)
10		vj	. . . . . . . . . . 11 setvar 𝑗
11	10	cv 1363	. . . . . . . . . 10 class 𝑗
12	11, 1	wcel 2160	. . . . . . . . 9 wff 𝑗 ∈ 𝐴
13	12	wdc 835	. . . . . . . 8 wff DECID 𝑗 ∈ 𝐴
14	13, 10, 8	wral 2468	. . . . . . 7 wff ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴
15	9, 14	wa 104	. . . . . 6 wff (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
16		vy	. . . . . . . . . . . 12 setvar 𝑦
17	16	cv 1363	. . . . . . . . . . 11 class 𝑦
18		cc0 7829	. . . . . . . . . . 11 class 0
19		cap 8556	. . . . . . . . . . 11 class #
20	17, 18, 19	wbr 4018	. . . . . . . . . 10 wff 𝑦 # 0
21		cmul 7834	. . . . . . . . . . . 12 class ·
22		cz 9271	. . . . . . . . . . . . 13 class ℤ
23	3	cv 1363	. . . . . . . . . . . . . . 15 class 𝑘
24	23, 1	wcel 2160	. . . . . . . . . . . . . 14 wff 𝑘 ∈ 𝐴
25		c1 7830	. . . . . . . . . . . . . 14 class 1
26	24, 2, 25	cif 3549	. . . . . . . . . . . . 13 class if(𝑘 ∈ 𝐴, 𝐵, 1)
27	3, 22, 26	cmpt 4079	. . . . . . . . . . . 12 class (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
28		vn	. . . . . . . . . . . . 13 setvar 𝑛
29	28	cv 1363	. . . . . . . . . . . 12 class 𝑛
30	21, 27, 29	cseq 10463	. . . . . . . . . . 11 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
31		cli 11304	. . . . . . . . . . 11 class ⇝
32	30, 17, 31	wbr 4018	. . . . . . . . . 10 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦
33	20, 32	wa 104	. . . . . . . . 9 wff (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
34	33, 16	wex 1503	. . . . . . . 8 wff ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
35	34, 28, 8	wrex 2469	. . . . . . 7 wff ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦)
36	21, 27, 6	cseq 10463	. . . . . . . 8 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)))
37		vx	. . . . . . . . 9 setvar 𝑥
38	37	cv 1363	. . . . . . . 8 class 𝑥
39	36, 38, 31	wbr 4018	. . . . . . 7 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥
40	35, 39	wa 104	. . . . . 6 wff (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)
41	15, 40	wa 104	. . . . 5 wff ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
42	41, 5, 22	wrex 2469	. . . 4 wff ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥))
43		cfz 10026	. . . . . . . . 9 class ...
44	25, 6, 43	co 5891	. . . . . . . 8 class (1...𝑚)
45		vf	. . . . . . . . 9 setvar 𝑓
46	45	cv 1363	. . . . . . . 8 class 𝑓
47	44, 1, 46	wf1o 5230	. . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto→𝐴
48		cn 8937	. . . . . . . . . . 11 class ℕ
49		cle 8011	. . . . . . . . . . . . 13 class ≤
50	29, 6, 49	wbr 4018	. . . . . . . . . . . 12 wff 𝑛 ≤ 𝑚
51	29, 46	cfv 5231	. . . . . . . . . . . . 13 class (𝑓‘𝑛)
52	3, 51, 2	csb 3072	. . . . . . . . . . . 12 class ⦋(𝑓‘𝑛) / 𝑘⦌𝐵
53	50, 52, 25	cif 3549	. . . . . . . . . . 11 class if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)
54	28, 48, 53	cmpt 4079	. . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))
55	21, 54, 25	cseq 10463	. . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))
56	6, 55	cfv 5231	. . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)
57	38, 56	wceq 1364	. . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)
58	47, 57	wa 104	. . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
59	58, 45	wex 1503	. . . . 5 wff ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
60	59, 5, 48	wrex 2469	. . . 4 wff ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))
61	42, 60	wo 709	. . 3 wff (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)))
62	61, 37	cio 5191	. 2 class (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
63	4, 62	wceq 1364	1 wff ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))

This definition is referenced by:  prodeq1f  11578  nfcprod1  11580  nfcprod  11581  prodeq2w  11582  prodeq2  11583  cbvprod  11584  zproddc  11605  fprodseq  11609