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 15940
Description: Define the product of a series with an index set of integers 𝐴. This definition takes most of the aspects of df-sum 15723 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 15939 . 2 class 𝑘𝐴 𝐵
5 vm . . . . . . . . 9 setvar 𝑚
65cv 1539 . . . . . . . 8 class 𝑚
7 cuz 12878 . . . . . . . 8 class
86, 7cfv 6561 . . . . . . 7 class (ℤ𝑚)
91, 8wss 3951 . . . . . 6 wff 𝐴 ⊆ (ℤ𝑚)
10 vy . . . . . . . . . . 11 setvar 𝑦
1110cv 1539 . . . . . . . . . 10 class 𝑦
12 cc0 11155 . . . . . . . . . 10 class 0
1311, 12wne 2940 . . . . . . . . 9 wff 𝑦 ≠ 0
14 cmul 11160 . . . . . . . . . . 11 class ·
15 cz 12613 . . . . . . . . . . . 12 class
163cv 1539 . . . . . . . . . . . . . 14 class 𝑘
1716, 1wcel 2108 . . . . . . . . . . . . 13 wff 𝑘𝐴
18 c1 11156 . . . . . . . . . . . . 13 class 1
1917, 2, 18cif 4525 . . . . . . . . . . . 12 class if(𝑘𝐴, 𝐵, 1)
203, 15, 19cmpt 5225 . . . . . . . . . . 11 class (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))
21 vn . . . . . . . . . . . 12 setvar 𝑛
2221cv 1539 . . . . . . . . . . 11 class 𝑛
2314, 20, 22cseq 14042 . . . . . . . . . 10 class seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
24 cli 15520 . . . . . . . . . 10 class
2523, 11, 24wbr 5143 . . . . . . . . 9 wff seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦
2613, 25wa 395 . . . . . . . 8 wff (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2726, 10wex 1779 . . . . . . 7 wff 𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2827, 21, 8wrex 3070 . . . . . 6 wff 𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦)
2914, 20, 6cseq 14042 . . . . . . 7 class seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1)))
30 vx . . . . . . . 8 setvar 𝑥
3130cv 1539 . . . . . . 7 class 𝑥
3229, 31, 24wbr 5143 . . . . . 6 wff seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥
339, 28, 32w3a 1087 . . . . 5 wff (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
3433, 5, 15wrex 3070 . . . 4 wff 𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥)
35 cfz 13547 . . . . . . . . 9 class ...
3618, 6, 35co 7431 . . . . . . . 8 class (1...𝑚)
37 vf . . . . . . . . 9 setvar 𝑓
3837cv 1539 . . . . . . . 8 class 𝑓
3936, 1, 38wf1o 6560 . . . . . . 7 wff 𝑓:(1...𝑚)–1-1-onto𝐴
40 cn 12266 . . . . . . . . . . 11 class
4122, 38cfv 6561 . . . . . . . . . . . 12 class (𝑓𝑛)
423, 41, 2csb 3899 . . . . . . . . . . 11 class (𝑓𝑛) / 𝑘𝐵
4321, 40, 42cmpt 5225 . . . . . . . . . 10 class (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
4414, 43, 18cseq 14042 . . . . . . . . 9 class seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))
456, 44cfv 6561 . . . . . . . 8 class (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4631, 45wceq 1540 . . . . . . 7 wff 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)
4739, 46wa 395 . . . . . 6 wff (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4847, 37wex 1779 . . . . 5 wff 𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
4948, 5, 40wrex 3070 . . . 4 wff 𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))
5034, 49wo 848 . . 3 wff (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
5150, 30cio 6512 . 2 class (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
524, 51wceq 1540 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  15941  prodeq1f  15942  prodeq1  15943  nfcprod1  15944  nfcprod  15945  prodeq2w  15946  prodeq2ii  15947  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  prodeq2sdv  15959  zprod  15973  fprod  15977  prodeq2si  36205  prodeq12sdv  36219  cbvprodvw2  36248  cbvproddavw  36281  cbvproddavw2  36297
  Copyright terms: Public domain W3C validator