Metamath Proof Explorer

Definition df-prod

Description: Define the product of a series with an index set of integers A . This definition takes most of the aspects of df-sum 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)

Ref Expression
Assertion df-prod ⊢ ∏ k ∈ A B = ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 vk setvar k
1 cA class A
2 cB class B
3 1 2 0 cprod class ∏ k ∈ A B
4 vx setvar x
5 vm setvar m
6 cz class ℤ
7 cuz class ℤ ≥
8 5 cv setvar m
9 8 7 cfv class ℤ ≥ m
10 1 9 wss wff A ⊆ ℤ ≥ m
11 vn setvar n
12 vy setvar y
13 12 cv setvar y
14 cc0 class 0
15 13 14 wne wff y ≠ 0
16 11 cv setvar n
17 cmul class ×
18 0 cv setvar k
19 18 1 wcel wff k ∈ A
20 c1 class 1
21 19 2 20 cif class if k ∈ A B 1
22 0 6 21 cmpt class k ∈ ℤ ⟼ if k ∈ A B 1
23 17 22 16 cseq class seq n × k ∈ ℤ ⟼ if k ∈ A B 1
24 cli class ⇝
25 23 13 24 wbr wff seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
26 15 25 wa wff y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
27 26 12 wex wff ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
28 27 11 9 wrex wff ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y
29 17 22 8 cseq class seq m × k ∈ ℤ ⟼ if k ∈ A B 1
30 4 cv setvar x
31 29 30 24 wbr wff seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x
32 10 28 31 w3a wff A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x
33 32 5 6 wrex wff ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x
34 cn class ℕ
35 vf setvar f
36 35 cv setvar f
37 cfz class …
38 20 8 37 co class 1 … m
39 38 1 36 wf1o wff f : 1 … m ⟶ 1-1 onto A
40 16 36 cfv class f ⁡ n
41 0 40 2 csb class ⦋ f ⁡ n / k⦌ B
42 11 34 41 cmpt class n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
43 17 42 20 cseq class seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B
44 8 43 cfv class seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
45 30 44 wceq wff x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
46 39 45 wa wff f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
47 46 35 wex wff ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
48 47 5 34 wrex wff ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
49 33 48 wo wff ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
50 49 4 cio class ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m
51 3 50 wceq wff ∏ k ∈ A B = ι x | ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ∨ ∃ m ∈ ℕ ∃ f f : 1 … m ⟶ 1-1 onto A ∧ x = seq 1 × n ∈ ℕ ⟼ ⦋ f ⁡ n / k⦌ B ⁡ m