MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-prod Structured version   Visualization version   GIF version

Definition df-prod 15626
Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15408 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3cprod 15625 . 2 class 𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1538 . . . . . . . 8 class 𝑚
7 cuz 12592 . . . . . . . 8 class
86, 7cfv 6426 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3886 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 vy . . . . . . . . . . 11 setvar 𝑦
1110cv 1538 . . . . . . . . . 10 class 𝑦
12 cc0 10881 . . . . . . . . . 10 class 0
1311, 12wne 2943 . . . . . . . . 9 wff 𝑦 ≠ 0
14 cmul 10886 . . . . . . . . . . 11 class ·
15 cz 12329 . . . . . . . . . . . 12 class
163cv 1538 . . . . . . . . . . . . . 14 class 𝑘
1716, 1wcel 2106 . . . . . . . . . . . . 13 wff 𝑘𝐴
18 c1 10882 . . . . . . . . . . . . 13 class 1
1917, 2, 18cif 4459 . . . . . . . . . . . 12 class if(𝑘𝐴, 𝐵, 1)
203, 15, 19cmpt 5156 . . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
21 vn . . . . . . . . . . . 12 setvar 𝑛
2221cv 1538 . . . . . . . . . . 11 class 𝑛
2314, 20, 22cseq 13731 . . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
24 cli 15203 . . . . . . . . . 10 class
2523, 11, 24wbr 5073 . . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
2613, 25wa 396 . . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2726, 10wex 1782 . . . . . . 7 wff 𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2827, 21, 8wrex 3065 . . . . . 6 wff 𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2914, 20, 6cseq 13731 . . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
30 vx . . . . . . . 8 setvar 𝑥
3130cv 1538 . . . . . . 7 class 𝑥
3229, 31, 24wbr 5073 . . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥
339, 28, 32w3a 1086 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
3433, 5, 15wrex 3065 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
35 cfz 13249 . . . . . . . . 9 class ...
3618, 6, 35co 7267 . . . . . . . 8 class (1...𝑚)
37 vf . . . . . . . . 9 setvar 𝑓
3837cv 1538 . . . . . . . 8 class 𝑓
3936, 1, 38wf1o 6425 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
40 cn 11983 . . . . . . . . . . 11 class
4122, 38cfv 6426 . . . . . . . . . . . 12 class (𝑓𝑛)
423, 41, 2csb 3831 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
4321, 40, 42cmpt 5156 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
4414, 43, 18cseq 13731 . . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
456, 44cfv 6426 . . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4631, 45wceq 1539 . . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4739, 46wa 396 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4847, 37wex 1782 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4948, 5, 40wrex 3065 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
5034, 49wo 844 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
5150, 30cio 6382 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
524, 51wceq 1539 1 wff 𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
Colors of variables: wff setvar class
This definition is referenced by:  prodex  15627  prodeq1f  15628  nfcprod1  15630  nfcprod  15631  prodeq2w  15632  prodeq2ii  15633  cbvprod  15635  zprod  15657  fprod  15661
  Copyright terms: Public domain W3C validator