# 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

### 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
42 11 34 41 cmpt
43 17 42 20 cseq
44 8 43 cfv
45 30 44 wceq
46 39 45 wa
47 46 35 wex
48 47 5 34 wrex
49 33 48 wo
50 49 4 cio
51 3 50 wceq