zprod

Description: Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypotheses	zprod.1	$⊢ Z = ℤ_{\geq M}$
	zprod.2	$⊢ φ \to M \in ℤ$
	zprod.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
	zprod.4	$⊢ φ \to A \subseteq Z$
	zprod.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 1)$
	zprod.6	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	zprod	$⊢ φ \to \prod_{k \in A} B = ⇝ (seq M (\times F))$

Proof

Step	Hyp	Ref	Expression
1		zprod.1	$⊢ Z = ℤ_{\geq M}$
2		zprod.2	$⊢ φ \to M \in ℤ$
3		zprod.3	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
4		zprod.4	$⊢ φ \to A \subseteq Z$
5		zprod.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, B, 1)$
6		zprod.6	$⊢ (φ \land k \in A) \to B \in ℂ$
7		3simpb	$⊢ (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) \to (A \subseteq ℤ_{\geq m} \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
8		nfcv	$⊢ \underline{Ⅎ} i if (k \in A, B, 1)$
9		nfv	$⊢ Ⅎ k i \in A$
10		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ i / k ⦌ B$
11		nfcv	$⊢ \underline{Ⅎ} k 1$
12	9 10 11	nfif	$⊢ \underline{Ⅎ} k if (i \in A, ⦋ i / k ⦌ B, 1)$
13		eleq1w	$⊢ k = i \to (k \in A \leftrightarrow i \in A)$
14		csbeq1a	$⊢ k = i \to B = ⦋ i / k ⦌ B$
15	13 14	ifbieq1d	$⊢ k = i \to if (k \in A, B, 1) = if (i \in A, ⦋ i / k ⦌ B, 1)$
16	8 12 15	cbvmpt	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) = (i \in ℤ ⟼ if (i \in A, ⦋ i / k ⦌ B, 1))$
17		simpll	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to φ$
18	6	ralrimiva	$⊢ φ \to \forall k \in A B \in ℂ$
19	10	nfel1	$⊢ Ⅎ k ⦋ i / k ⦌ B \in ℂ$
20	14	eleq1d	$⊢ k = i \to (B \in ℂ \leftrightarrow ⦋ i / k ⦌ B \in ℂ)$
21	19 20	rspc	$⊢ i \in A \to (\forall k \in A B \in ℂ \to ⦋ i / k ⦌ B \in ℂ)$
22	18 21	syl5	$⊢ i \in A \to (φ \to ⦋ i / k ⦌ B \in ℂ)$
23	17 22	mpan9	$⊢ (((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \land i \in A) \to ⦋ i / k ⦌ B \in ℂ$
24		simplr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to m \in ℤ$
25	2	ad2antrr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to M \in ℤ$
26		simpr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to A \subseteq ℤ_{\geq m}$
27	4 1	sseqtrdi	$⊢ φ \to A \subseteq ℤ_{\geq M}$
28	27	ad2antrr	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to A \subseteq ℤ_{\geq M}$
29	16 23 24 25 26 28	prodrb	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to (seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \leftrightarrow seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
30	29	biimpd	$⊢ ((φ \land m \in ℤ) \land A \subseteq ℤ_{\geq m}) \to (seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
31	30	expimpd	$⊢ (φ \land m \in ℤ) \to ((A \subseteq ℤ_{\geq m} \land seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
32	7 31	syl5	$⊢ (φ \land m \in ℤ) \to ((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) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
33	32	rexlimdva	$⊢ φ \to (\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) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
34		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
35		zssre	$⊢ ℤ \subseteq ℝ$
36	34 35	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
37	1 36	eqsstri	$⊢ Z \subseteq ℝ$
38	4 37	sstrdi	$⊢ φ \to A \subseteq ℝ$
39	38	ad2antrr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \subseteq ℝ$
40		ltso	$⊢ < Or ℝ$
41		soss	$⊢ A \subseteq ℝ \to (< Or ℝ \to < Or A)$
42	39 40 41	mpisyl	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to < Or A$
43		fzfi	$⊢ (1 \dots m) \in Fin$
44		ovex	$⊢ (1 \dots m) \in V$
45	44	f1oen	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to (1 \dots m) \approx A$
46	45	adantl	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (1 \dots m) \approx A$
47	46	ensymd	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \approx (1 \dots m)$
48		enfii	$⊢ ((1 \dots m) \in Fin \land A \approx (1 \dots m)) \to A \in Fin$
49	43 47 48	sylancr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to A \in Fin$
50		fz1iso	$⊢ (< Or A \land A \in Fin) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
51	42 49 50	syl2anc	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to \exists g g {Isom}_{<, <} ((1 \dots \|A\|), A)$
52		simpll	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to φ$
53	52 22	mpan9	$⊢ (((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \land i \in A) \to ⦋ i / k ⦌ B \in ℂ$
54		fveq2	$⊢ n = j \to f (n) = f (j)$
55	54	csbeq1d	$⊢ n = j \to ⦋ f (n) / k ⦌ B = ⦋ f (j) / k ⦌ B$
56		csbcow	$⊢ ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B = ⦋ f (j) / k ⦌ B$
57	55 56	eqtr4di	$⊢ n = j \to ⦋ f (n) / k ⦌ B = ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B$
58	57	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (j \in ℕ ⟼ ⦋ f (j) / i ⦌ ⦋ i / k ⦌ B)$
59		eqid	$⊢ (j \in ℕ ⟼ ⦋ g (j) / i ⦌ ⦋ i / k ⦌ B) = (j \in ℕ ⟼ ⦋ g (j) / i ⦌ ⦋ i / k ⦌ B)$
60		simplr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to m \in ℕ$
61	2	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to M \in ℤ$
62	27	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to A \subseteq ℤ_{\geq M}$
63		simprl	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to f : (1 \dots m) \underset{1-1 onto}{⟶} A$
64		simprr	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to g {Isom}_{<, <} ((1 \dots \|A\|), A)$
65	16 53 58 59 60 61 62 63 64	prodmolem2a	$⊢ ((φ \land m \in ℕ) \land (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land g {Isom}_{<, <} ((1 \dots \|A\|), A))) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
66	65	expr	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
67	66	exlimdv	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (\exists g g {Isom}_{<, <} ((1 \dots \|A\|), A) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
68	51 67	mpd	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)$
69		breq2	$⊢ x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \to (seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \leftrightarrow seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
70	68 69	syl5ibrcom	$⊢ ((φ \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
71	70	expimpd	$⊢ (φ \land m \in ℕ) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
72	71	exlimdv	$⊢ (φ \land m \in ℕ) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
73	72	rexlimdva	$⊢ φ \to (\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)) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
74	33 73	jaod	$⊢ φ \to ((\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))) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
75	2	adantr	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to M \in ℤ$
76	4	adantr	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to A \subseteq Z$
77	1	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
78		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
79	78	adantl	$⊢ (φ \land n \in ℤ_{\geq M}) \to n \in ℤ$
80		uztrn	$⊢ (z \in ℤ_{\geq n} \land n \in ℤ_{\geq M}) \to z \in ℤ_{\geq M}$
81	80	ancoms	$⊢ (n \in ℤ_{\geq M} \land z \in ℤ_{\geq n}) \to z \in ℤ_{\geq M}$
82	1	eleq2i	$⊢ k \in Z \leftrightarrow k \in ℤ_{\geq M}$
83	1 34	eqsstri	$⊢ Z \subseteq ℤ$
84	83	sseli	$⊢ k \in Z \to k \in ℤ$
85		iftrue	$⊢ k \in A \to if (k \in A, B, 1) = B$
86	85	adantl	$⊢ (φ \land k \in A) \to if (k \in A, B, 1) = B$
87	86 6	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, B, 1) \in ℂ$
88	87	ex	$⊢ φ \to (k \in A \to if (k \in A, B, 1) \in ℂ)$
89		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 1) = 1$
90		ax-1cn	$⊢ 1 \in ℂ$
91	89 90	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 1) \in ℂ$
92	88 91	pm2.61d1	$⊢ φ \to if (k \in A, B, 1) \in ℂ$
93		eqid	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, B, 1))$
94	93	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 1) \in ℂ) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = if (k \in A, B, 1)$
95	84 92 94	syl2anr	$⊢ (φ \land k \in Z) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = if (k \in A, B, 1)$
96	5 95	eqtr4d	$⊢ (φ \land k \in Z) \to F (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (k)$
97	82 96	sylan2br	$⊢ (φ \land k \in ℤ_{\geq M}) \to F (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (k)$
98	97	ralrimiva	$⊢ φ \to \forall k \in ℤ_{\geq M} F (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (k)$
99		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
100	99	nfeq2	$⊢ Ⅎ k F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
101		fveq2	$⊢ k = z \to F (k) = F (z)$
102		fveq2	$⊢ k = z \to (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
103	101 102	eqeq12d	$⊢ k = z \to (F (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (k) \leftrightarrow F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z))$
104	100 103	rspc	$⊢ z \in ℤ_{\geq M} \to (\forall k \in ℤ_{\geq M} F (k) = (k \in ℤ ⟼ if (k \in A, B, 1)) (k) \to F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z))$
105	98 104	mpan9	$⊢ (φ \land z \in ℤ_{\geq M}) \to F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
106	81 105	sylan2	$⊢ (φ \land (n \in ℤ_{\geq M} \land z \in ℤ_{\geq n})) \to F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
107	106	anassrs	$⊢ ((φ \land n \in ℤ_{\geq M}) \land z \in ℤ_{\geq n}) \to F (z) = (k \in ℤ ⟼ if (k \in A, B, 1)) (z)$
108	79 107	seqfeq	$⊢ (φ \land n \in ℤ_{\geq M}) \to seq n (\times F) = seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
109	108	breq1d	$⊢ (φ \land n \in ℤ_{\geq M}) \to (seq n (\times F) ⇝ y \leftrightarrow seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
110	109	anbi2d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y))$
111	110	exbidv	$⊢ (φ \land n \in ℤ_{\geq M}) \to (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y))$
112	77 111	sylan2b	$⊢ (φ \land n \in Z) \to (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y))$
113	112	rexbidva	$⊢ φ \to (\exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y))$
114	3 113	mpbid	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
115	114	adantr	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y)$
116		simpr	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x$
117		fveq2	$⊢ m = M \to ℤ_{\geq m} = ℤ_{\geq M}$
118	117 1	eqtr4di	$⊢ m = M \to ℤ_{\geq m} = Z$
119	118	sseq2d	$⊢ m = M \to (A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq Z)$
120	118	rexeqdv	$⊢ m = M \to (\exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow \exists n \in Z \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y))$
121		seqeq1	$⊢ m = M \to seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1)))$
122	121	breq1d	$⊢ m = M \to (seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \leftrightarrow seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
123	119 120 122	3anbi123d	$⊢ m = M \to ((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) \leftrightarrow (A \subseteq Z \land \exists n \in Z \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))$
124	123	rspcev	$⊢ (M \in ℤ \land (A \subseteq Z \land \exists n \in Z \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)) \to \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)$
125	75 76 115 116 124	syl13anc	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to \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)$
126	125	orcd	$⊢ (φ \land seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x) \to (\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)))$
127	126	ex	$⊢ φ \to (seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \to (\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))))$
128	74 127	impbid	$⊢ φ \to ((\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))) \leftrightarrow seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x)$
129	95 5	eqtr4d	$⊢ (φ \land k \in Z) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = F (k)$
130	82 129	sylan2br	$⊢ (φ \land k \in ℤ_{\geq M}) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = F (k)$
131	130	ralrimiva	$⊢ φ \to \forall k \in ℤ_{\geq M} (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = F (k)$
132	99	nfeq1	$⊢ Ⅎ k (k \in ℤ ⟼ if (k \in A, B, 1)) (z) = F (z)$
133	102 101	eqeq12d	$⊢ k = z \to ((k \in ℤ ⟼ if (k \in A, B, 1)) (k) = F (k) \leftrightarrow (k \in ℤ ⟼ if (k \in A, B, 1)) (z) = F (z))$
134	132 133	rspc	$⊢ z \in ℤ_{\geq M} \to (\forall k \in ℤ_{\geq M} (k \in ℤ ⟼ if (k \in A, B, 1)) (k) = F (k) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (z) = F (z))$
135	131 134	mpan9	$⊢ (φ \land z \in ℤ_{\geq M}) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (z) = F (z)$
136	2 135	seqfeq	$⊢ φ \to seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq M (\times F)$
137	136	breq1d	$⊢ φ \to (seq M (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \leftrightarrow seq M (\times F) ⇝ x)$
138	128 137	bitrd	$⊢ φ \to ((\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))) \leftrightarrow seq M (\times F) ⇝ x)$
139	138	iotabidv	$⊢ φ \to (ι 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)))) = (ι x \| seq M (\times F) ⇝ x)$
140		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))))$
141		df-fv	$⊢ ⇝ (seq M (\times F)) = (ι x \| seq M (\times F) ⇝ x)$
142	139 140 141	3eqtr4g	$⊢ φ \to \prod_{k \in A} B = ⇝ (seq M (\times F))$

Metamath Proof Explorer

Theorem zprod

Proof