fprod

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017)

	Ref	Expression
Hypotheses	fprod.1	$⊢ k = F (n) \to B = C$
	fprod.2	$⊢ φ \to M \in ℕ$
	fprod.3	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} A$
	fprod.4	$⊢ (φ \land k \in A) \to B \in ℂ$
	fprod.5	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = C$
Assertion	fprod	$⊢ φ \to \prod_{k \in A} B = seq 1 (\times G) (M)$

Proof

Step	Hyp	Ref	Expression
1		fprod.1	$⊢ k = F (n) \to B = C$
2		fprod.2	$⊢ φ \to M \in ℕ$
3		fprod.3	$⊢ φ \to F : (1 \dots M) \underset{1-1 onto}{⟶} A$
4		fprod.4	$⊢ (φ \land k \in A) \to B \in ℂ$
5		fprod.5	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = C$
6		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))))$
7		fvex	$⊢ seq 1 (\times G) (M) \in V$
8		nfcv	$⊢ \underline{Ⅎ} j if (k \in A, B, 1)$
9		nfv	$⊢ Ⅎ k j \in A$
10		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
11		nfcv	$⊢ \underline{Ⅎ} k 1$
12	9 10 11	nfif	$⊢ \underline{Ⅎ} k if (j \in A, ⦋ j / k ⦌ B, 1)$
13		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
14		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
15	13 14	ifbieq1d	$⊢ k = j \to if (k \in A, B, 1) = if (j \in A, ⦋ j / k ⦌ B, 1)$
16	8 12 15	cbvmpt	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) = (j \in ℤ ⟼ if (j \in A, ⦋ j / k ⦌ B, 1))$
17	4	ralrimiva	$⊢ φ \to \forall k \in A B \in ℂ$
18	10	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℂ$
19	14	eleq1d	$⊢ k = j \to (B \in ℂ \leftrightarrow ⦋ j / k ⦌ B \in ℂ)$
20	18 19	rspc	$⊢ j \in A \to (\forall k \in A B \in ℂ \to ⦋ j / k ⦌ B \in ℂ)$
21	17 20	mpan9	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in ℂ$
22		fveq2	$⊢ n = i \to f (n) = f (i)$
23	22	csbeq1d	$⊢ n = i \to ⦋ f (n) / k ⦌ B = ⦋ f (i) / k ⦌ B$
24		csbcow	$⊢ ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B = ⦋ f (i) / k ⦌ B$
25	23 24	eqtr4di	$⊢ n = i \to ⦋ f (n) / k ⦌ B = ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B$
26	25	cbvmptv	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (i \in ℕ ⟼ ⦋ f (i) / j ⦌ ⦋ j / k ⦌ B)$
27	16 21 26	prodmo	$⊢ φ \to \exists^{*} 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)))$
28		f1of	$⊢ F : (1 \dots M) \underset{1-1 onto}{⟶} A \to F : (1 \dots M) ⟶ A$
29	3 28	syl	$⊢ φ \to F : (1 \dots M) ⟶ A$
30		ovex	$⊢ (1 \dots M) \in V$
31		fex	$⊢ (F : (1 \dots M) ⟶ A \land (1 \dots M) \in V) \to F \in V$
32	29 30 31	sylancl	$⊢ φ \to F \in V$
33		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
34	2 33	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
35		elfznn	$⊢ n \in (1 \dots M) \to n \in ℕ$
36		fvex	$⊢ G (n) \in V$
37	5 36	eqeltrrdi	$⊢ (φ \land n \in (1 \dots M)) \to C \in V$
38		eqid	$⊢ (n \in ℕ ⟼ C) = (n \in ℕ ⟼ C)$
39	38	fvmpt2	$⊢ (n \in ℕ \land C \in V) \to (n \in ℕ ⟼ C) (n) = C$
40	35 37 39	syl2an2	$⊢ (φ \land n \in (1 \dots M)) \to (n \in ℕ ⟼ C) (n) = C$
41	5 40	eqtr4d	$⊢ (φ \land n \in (1 \dots M)) \to G (n) = (n \in ℕ ⟼ C) (n)$
42	41	ralrimiva	$⊢ φ \to \forall n \in (1 \dots M) G (n) = (n \in ℕ ⟼ C) (n)$
43		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ C) (k)$
44	43	nfeq2	$⊢ Ⅎ n G (k) = (n \in ℕ ⟼ C) (k)$
45		fveq2	$⊢ n = k \to G (n) = G (k)$
46		fveq2	$⊢ n = k \to (n \in ℕ ⟼ C) (n) = (n \in ℕ ⟼ C) (k)$
47	45 46	eqeq12d	$⊢ n = k \to (G (n) = (n \in ℕ ⟼ C) (n) \leftrightarrow G (k) = (n \in ℕ ⟼ C) (k))$
48	44 47	rspc	$⊢ k \in (1 \dots M) \to (\forall n \in (1 \dots M) G (n) = (n \in ℕ ⟼ C) (n) \to G (k) = (n \in ℕ ⟼ C) (k))$
49	42 48	mpan9	$⊢ (φ \land k \in (1 \dots M)) \to G (k) = (n \in ℕ ⟼ C) (k)$
50	34 49	seqfveq	$⊢ φ \to seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ C)) (M)$
51	3 50	jca	$⊢ φ \to (F : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ C)) (M))$
52		f1oeq1	$⊢ f = F \to (f : (1 \dots M) \underset{1-1 onto}{⟶} A \leftrightarrow F : (1 \dots M) \underset{1-1 onto}{⟶} A)$
53		fveq1	$⊢ f = F \to f (n) = F (n)$
54	53	csbeq1d	$⊢ f = F \to ⦋ f (n) / k ⦌ B = ⦋ F (n) / k ⦌ B$
55		fvex	$⊢ F (n) \in V$
56	55 1	csbie	$⊢ ⦋ F (n) / k ⦌ B = C$
57	54 56	eqtrdi	$⊢ f = F \to ⦋ f (n) / k ⦌ B = C$
58	57	mpteq2dv	$⊢ f = F \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ C)$
59	58	seqeq3d	$⊢ f = F \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) = seq 1 (\times (n \in ℕ ⟼ C))$
60	59	fveq1d	$⊢ f = F \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M) = seq 1 (\times (n \in ℕ ⟼ C)) (M)$
61	60	eqeq2d	$⊢ f = F \to (seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M) \leftrightarrow seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ C)) (M))$
62	52 61	anbi12d	$⊢ f = F \to ((f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)) \leftrightarrow (F : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ C)) (M)))$
63	32 51 62	spcedv	$⊢ φ \to \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))$
64		oveq2	$⊢ m = M \to (1 \dots m) = (1 \dots M)$
65	64	f1oeq2d	$⊢ m = M \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots M) \underset{1-1 onto}{⟶} A)$
66		fveq2	$⊢ m = M \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)$
67	66	eqeq2d	$⊢ m = M \to (seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))$
68	65 67	anbi12d	$⊢ m = M \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)))$
69	68	exbidv	$⊢ m = M \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M)))$
70	69	rspcev	$⊢ (M \in ℕ \land \exists f (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (M))) \to \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
71	2 63 70	syl2anc	$⊢ φ \to \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
72	71	olcd	$⊢ φ \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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
73		breq2	$⊢ x = seq 1 (\times G) (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 G) (M))$
74	73	3anbi3d	$⊢ x = seq 1 (\times G) (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 ℤ_{\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))) ⇝ seq 1 (\times G) (M)))$
75	74	rexbidv	$⊢ x = seq 1 (\times G) (M) \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) \leftrightarrow \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))) ⇝ seq 1 (\times G) (M)))$
76		eqeq1	$⊢ x = seq 1 (\times G) (M) \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))$
77	76	anbi2d	$⊢ x = seq 1 (\times G) (M) \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
78	77	exbidv	$⊢ x = seq 1 (\times G) (M) \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
79	78	rexbidv	$⊢ x = seq 1 (\times G) (M) \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)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))$
80	75 79	orbi12d	$⊢ x = seq 1 (\times G) (M) \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 (\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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))$
81	80	moi2	$⊢ ((seq 1 (\times G) (M) \in V \land \exists^{*} 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)))) \land ((\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))) \land (\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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))) \to x = seq 1 (\times G) (M)$
82	7 81	mpanl1	$⊢ (\exists^{*} 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))) \land ((\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))) \land (\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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))))) \to x = seq 1 (\times G) (M)$
83	82	ancom2s	$⊢ (\exists^{*} 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))) \land ((\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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m))) \land (\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 x = seq 1 (\times G) (M)$
84	83	expr	$⊢ (\exists^{*} 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))) \land (\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))) ⇝ seq 1 (\times G) (M)) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land seq 1 (\times G) (M) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)))) \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 x = seq 1 (\times G) (M))$
85	27 72 84	syl2anc	$⊢ φ \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 x = seq 1 (\times G) (M))$
86	72 80	syl5ibrcom	$⊢ φ \to (x = seq 1 (\times G) (M) \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))))$
87	85 86	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 x = seq 1 (\times G) (M))$
88	87	adantr	$⊢ (φ \land seq 1 (\times G) (M) \in V) \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 x = seq 1 (\times G) (M))$
89	88	iota5	$⊢ (φ \land seq 1 (\times G) (M) \in V) \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)))) = seq 1 (\times G) (M)$
90	7 89	mpan2	$⊢ φ \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)))) = seq 1 (\times G) (M)$
91	6 90	syl5eq	$⊢ φ \to \prod_{k \in A} B = seq 1 (\times G) (M)$

Metamath Proof Explorer

Theorem fprod

Proof