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	$⊢ \prod_{k \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ 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 \prod_{k \in A} B$
4		vx	$setvar x$
5		vm	$setvar m$
6		cz	$class ℤ$
7		cuz	$class ℤ_{\geq}$
8	5	cv	$setvar m$
9	8 7	cfv	$class ℤ_{\geq m}$
10	1 9	wss	$wff A \subseteq ℤ_{\geq m}$
11		vn	$setvar n$
12		vy	$setvar y$
13	12	cv	$setvar y$
14		cc0	$class 0$
15	13 14	wne	$wff y \neq 0$
16	11	cv	$setvar n$
17		cmul	$class \times$
18	0	cv	$setvar k$
19	18 1	wcel	$wff k \in A$
20		c1	$class 1$
21	19 2 20	cif	$class if (k \in A, B, 1)$
22	0 6 21	cmpt	$class (k \in ℤ ⟼ if (k \in A, B, 1))$
23	17 22 16	cseq	$class seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
24		cli	$class ⇝$
25	23 13 24	wbr	$wff seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y$
26	15 25	wa	$wff (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
27	26 12	wex	$wff \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
28	27 11 9	wrex	$wff \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
29	17 22 8	cseq	$class seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
30	4	cv	$setvar x$
31	29 30 24	wbr	$wff seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x$
32	10 28 31	w3a	$wff (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
33	32 5 6	wrex	$wff \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
34		cn	$class ℕ$
35		vf	$setvar f$
36	35	cv	$setvar f$
37		cfz	$class \dots$
38	20 8 37	co	$class (1 \dots m)$
39	38 1 36	wf1o	$wff f : (1 \dots m) \underset{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 \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
43	17 42 20	cseq	$class seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B))$
44	8 43	cfv	$class seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
45	30 44	wceq	$wff x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
46	39 45	wa	$wff (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
47	46 35	wex	$wff \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
48	47 5 34	wrex	$wff \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
49	33 48	wo	$wff (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
50	49 4	cio	$class (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
51	3 50	wceq	$wff \prod_{k \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$

Metamath Proof Explorer

Definition df-prod

Detailed syntax breakdown