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 15936
Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15719 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 15935 . 2 class 𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1535 . . . . . . . 8 class 𝑚
7 cuz 12875 . . . . . . . 8 class
86, 7cfv 6562 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3962 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 vy . . . . . . . . . . 11 setvar 𝑦
1110cv 1535 . . . . . . . . . 10 class 𝑦
12 cc0 11152 . . . . . . . . . 10 class 0
1311, 12wne 2937 . . . . . . . . 9 wff 𝑦 ≠ 0
14 cmul 11157 . . . . . . . . . . 11 class ·
15 cz 12610 . . . . . . . . . . . 12 class
163cv 1535 . . . . . . . . . . . . . 14 class 𝑘
1716, 1wcel 2105 . . . . . . . . . . . . 13 wff 𝑘𝐴
18 c1 11153 . . . . . . . . . . . . 13 class 1
1917, 2, 18cif 4530 . . . . . . . . . . . 12 class if(𝑘𝐴, 𝐵, 1)
203, 15, 19cmpt 5230 . . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
21 vn . . . . . . . . . . . 12 setvar 𝑛
2221cv 1535 . . . . . . . . . . 11 class 𝑛
2314, 20, 22cseq 14038 . . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
24 cli 15516 . . . . . . . . . 10 class
2523, 11, 24wbr 5147 . . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
2613, 25wa 395 . . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2726, 10wex 1775 . . . . . . 7 wff 𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2827, 21, 8wrex 3067 . . . . . 6 wff 𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2914, 20, 6cseq 14038 . . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
30 vx . . . . . . . 8 setvar 𝑥
3130cv 1535 . . . . . . 7 class 𝑥
3229, 31, 24wbr 5147 . . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥
339, 28, 32w3a 1086 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
3433, 5, 15wrex 3067 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
35 cfz 13543 . . . . . . . . 9 class ...
3618, 6, 35co 7430 . . . . . . . 8 class (1...𝑚)
37 vf . . . . . . . . 9 setvar 𝑓
3837cv 1535 . . . . . . . 8 class 𝑓
3936, 1, 38wf1o 6561 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
40 cn 12263 . . . . . . . . . . 11 class
4122, 38cfv 6562 . . . . . . . . . . . 12 class (𝑓𝑛)
423, 41, 2csb 3907 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
4321, 40, 42cmpt 5230 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
4414, 43, 18cseq 14038 . . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
456, 44cfv 6562 . . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4631, 45wceq 1536 . . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4739, 46wa 395 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4847, 37wex 1775 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4948, 5, 40wrex 3067 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
5034, 49wo 847 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
5150, 30cio 6513 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
524, 51wceq 1536 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  15937  prodeq1f  15938  prodeq1  15939  nfcprod1  15940  nfcprod  15941  prodeq2w  15942  prodeq2ii  15943  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  prodeq2sdv  15955  zprod  15969  fprod  15973  prodeq2si  36185  prodeq12sdv  36200  cbvprodvw2  36229  cbvproddavw  36262  cbvproddavw2  36278
  Copyright terms: Public domain W3C validator