ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-proddc GIF version

Definition df-proddc 11332
Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sumdc 11135 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3cprod 11331 . 2 class 𝑘𝐴 𝐵
5 vm . . . . . . . . . 10 setvar 𝑚
65cv 1330 . . . . . . . . 9 class 𝑚
7 cuz 9338 . . . . . . . . 9 class
86, 7cfv 5123 . . . . . . . 8 class (ℤ𝑚)
91, 8wss 3071 . . . . . . 7 wff 𝐴 ⊆ (ℤ𝑚)
10 vj . . . . . . . . . . 11 setvar 𝑗
1110cv 1330 . . . . . . . . . 10 class 𝑗
1211, 1wcel 1480 . . . . . . . . 9 wff 𝑗𝐴
1312wdc 819 . . . . . . . 8 wff DECID 𝑗𝐴
1413, 10, 8wral 2416 . . . . . . 7 wff 𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴
159, 14wa 103 . . . . . 6 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
16 vy . . . . . . . . . . . 12 setvar 𝑦
1716cv 1330 . . . . . . . . . . 11 class 𝑦
18 cc0 7632 . . . . . . . . . . 11 class 0
19 cap 8355 . . . . . . . . . . 11 class #
2017, 18, 19wbr 3929 . . . . . . . . . 10 wff 𝑦 # 0
21 cmul 7637 . . . . . . . . . . . 12 class ·
22 cz 9066 . . . . . . . . . . . . 13 class
233cv 1330 . . . . . . . . . . . . . . 15 class 𝑘
2423, 1wcel 1480 . . . . . . . . . . . . . 14 wff 𝑘𝐴
25 c1 7633 . . . . . . . . . . . . . 14 class 1
2624, 2, 25cif 3474 . . . . . . . . . . . . 13 class if(𝑘𝐴, 𝐵, 1)
273, 22, 26cmpt 3989 . . . . . . . . . . . 12 class (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
28 vn . . . . . . . . . . . . 13 setvar 𝑛
2928cv 1330 . . . . . . . . . . . 12 class 𝑛
3021, 27, 29cseq 10230 . . . . . . . . . . 11 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
31 cli 11059 . . . . . . . . . . 11 class
3230, 17, 31wbr 3929 . . . . . . . . . 10 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
3320, 32wa 103 . . . . . . . . 9 wff (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
3433, 16wex 1468 . . . . . . . 8 wff 𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
3534, 28, 8wrex 2417 . . . . . . 7 wff 𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
3621, 27, 6cseq 10230 . . . . . . . 8 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
37 vx . . . . . . . . 9 setvar 𝑥
3837cv 1330 . . . . . . . 8 class 𝑥
3936, 38, 31wbr 3929 . . . . . . 7 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥
4035, 39wa 103 . . . . . 6 wff (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
4115, 40wa 103 . . . . 5 wff ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
4241, 5, 22wrex 2417 . . . 4 wff 𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥))
43 cfz 9802 . . . . . . . . 9 class ...
4425, 6, 43co 5774 . . . . . . . 8 class (1...𝑚)
45 vf . . . . . . . . 9 setvar 𝑓
4645cv 1330 . . . . . . . 8 class 𝑓
4744, 1, 46wf1o 5122 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
48 cn 8732 . . . . . . . . . . 11 class
49 cle 7813 . . . . . . . . . . . . 13 class
5029, 6, 49wbr 3929 . . . . . . . . . . . 12 wff 𝑛𝑚
5129, 46cfv 5123 . . . . . . . . . . . . 13 class (𝑓𝑛)
523, 51, 2csb 3003 . . . . . . . . . . . 12 class (𝑓𝑛) / 𝑘𝐵
5350, 52, 25cif 3474 . . . . . . . . . . 11 class if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)
5428, 48, 53cmpt 3989 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1))
5521, 54, 25cseq 10230 . . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))
566, 55cfv 5123 . . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)
5738, 56wceq 1331 . . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)
5847, 57wa 103 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
5958, 45wex 1468 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
6059, 5, 48wrex 2417 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))
6142, 60wo 697 . . 3 wff (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚)))
6261, 37cio 5086 . 2 class (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
634, 62wceq 1331 1 wff 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 1)))‘𝑚))))
Colors of variables: wff set class
This definition is referenced by:  prodeq1f  11333  nfcprod1  11335  nfcprod  11336  prodeq2w  11337  prodeq2  11338  cbvprod  11339
  Copyright terms: Public domain W3C validator