prodmolem2a

	Ref	Expression
Hypotheses	prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
	prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	prodmo.3	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
	prodmolem2.4	$⊢ H = (j \in ℕ ⟼ ⦋ K (j) / k ⦌ B)$
	prodmolem2.5	$⊢ φ \to N \in ℕ$
	prodmolem2.6	$⊢ φ \to M \in ℤ$
	prodmolem2.7	$⊢ φ \to A \subseteq ℤ_{\geq M}$
	prodmolem2.8	$⊢ φ \to f : (1 \dots N) \underset{1-1 onto}{⟶} A$
	prodmolem2.9	$⊢ φ \to K {Isom}_{<, <} ((1 \dots \|A\|), A)$
Assertion	prodmolem2a	$⊢ φ \to seq M (\times F) ⇝ seq 1 (\times G) (N)$

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
2		prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodmo.3	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
4		prodmolem2.4	$⊢ H = (j \in ℕ ⟼ ⦋ K (j) / k ⦌ B)$
5		prodmolem2.5	$⊢ φ \to N \in ℕ$
6		prodmolem2.6	$⊢ φ \to M \in ℤ$
7		prodmolem2.7	$⊢ φ \to A \subseteq ℤ_{\geq M}$
8		prodmolem2.8	$⊢ φ \to f : (1 \dots N) \underset{1-1 onto}{⟶} A$
9		prodmolem2.9	$⊢ φ \to K {Isom}_{<, <} ((1 \dots \|A\|), A)$
10		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
11	10 8	hasheqf1od	$⊢ φ \to \|(1 \dots N)\| = \|A\|$
12	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
13		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
14	12 13	syl	$⊢ φ \to \|(1 \dots N)\| = N$
15	11 14	eqtr3d	$⊢ φ \to \|A\| = N$
16	15	oveq2d	$⊢ φ \to (1 \dots \|A\|) = (1 \dots N)$
17		isoeq4	$⊢ (1 \dots \|A\|) = (1 \dots N) \to (K {Isom}_{<, <} ((1 \dots \|A\|), A) \leftrightarrow K {Isom}_{<, <} ((1 \dots N), A))$
18	16 17	syl	$⊢ φ \to (K {Isom}_{<, <} ((1 \dots \|A\|), A) \leftrightarrow K {Isom}_{<, <} ((1 \dots N), A))$
19	9 18	mpbid	$⊢ φ \to K {Isom}_{<, <} ((1 \dots N), A)$
20		isof1o	$⊢ K {Isom}_{<, <} ((1 \dots N), A) \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
21		f1of	$⊢ K : (1 \dots N) \underset{1-1 onto}{⟶} A \to K : (1 \dots N) ⟶ A$
22	19 20 21	3syl	$⊢ φ \to K : (1 \dots N) ⟶ A$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	5 23	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
25		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
26	24 25	syl	$⊢ φ \to N \in (1 \dots N)$
27	22 26	ffvelcdmd	$⊢ φ \to K (N) \in A$
28	7 27	sseldd	$⊢ φ \to K (N) \in ℤ_{\geq M}$
29	7	sselda	$⊢ (φ \land j \in A) \to j \in ℤ_{\geq M}$
30	19 20	syl	$⊢ φ \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
31		f1ocnvfv2	$⊢ (K : (1 \dots N) \underset{1-1 onto}{⟶} A \land j \in A) \to K (K^{-1} (j)) = j$
32	30 31	sylan	$⊢ (φ \land j \in A) \to K (K^{-1} (j)) = j$
33		f1ocnv	$⊢ K : (1 \dots N) \underset{1-1 onto}{⟶} A \to K^{-1} : A \underset{1-1 onto}{⟶} (1 \dots N)$
34		f1of	$⊢ K^{-1} : A \underset{1-1 onto}{⟶} (1 \dots N) \to K^{-1} : A ⟶ (1 \dots N)$
35	30 33 34	3syl	$⊢ φ \to K^{-1} : A ⟶ (1 \dots N)$
36	35	ffvelcdmda	$⊢ (φ \land j \in A) \to K^{-1} (j) \in (1 \dots N)$
37		elfzle2	$⊢ K^{-1} (j) \in (1 \dots N) \to K^{-1} (j) \leq N$
38	36 37	syl	$⊢ (φ \land j \in A) \to K^{-1} (j) \leq N$
39	19	adantr	$⊢ (φ \land j \in A) \to K {Isom}_{<, <} ((1 \dots N), A)$
40		fzssuz	$⊢ (1 \dots N) \subseteq ℤ_{\geq 1}$
41		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
42		zssre	$⊢ ℤ \subseteq ℝ$
43	41 42	sstri	$⊢ ℤ_{\geq 1} \subseteq ℝ$
44	40 43	sstri	$⊢ (1 \dots N) \subseteq ℝ$
45		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
46	44 45	sstri	$⊢ (1 \dots N) \subseteq ℝ^{*}$
47	46	a1i	$⊢ (φ \land j \in A) \to (1 \dots N) \subseteq ℝ^{*}$
48		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
49	48 42	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
50	49 45	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ^{*}$
51	7 50	sstrdi	$⊢ φ \to A \subseteq ℝ^{*}$
52	51	adantr	$⊢ (φ \land j \in A) \to A \subseteq ℝ^{*}$
53	26	adantr	$⊢ (φ \land j \in A) \to N \in (1 \dots N)$
54		leisorel	$⊢ (K {Isom}_{<, <} ((1 \dots N), A) \land ((1 \dots N) \subseteq ℝ^{} \land A \subseteq ℝ^{}) \land (K^{-1} (j) \in (1 \dots N) \land N \in (1 \dots N))) \to (K^{-1} (j) \leq N \leftrightarrow K (K^{-1} (j)) \leq K (N))$
55	39 47 52 36 53 54	syl122anc	$⊢ (φ \land j \in A) \to (K^{-1} (j) \leq N \leftrightarrow K (K^{-1} (j)) \leq K (N))$
56	38 55	mpbid	$⊢ (φ \land j \in A) \to K (K^{-1} (j)) \leq K (N)$
57	32 56	eqbrtrrd	$⊢ (φ \land j \in A) \to j \leq K (N)$
58	7 48	sstrdi	$⊢ φ \to A \subseteq ℤ$
59	58	sselda	$⊢ (φ \land j \in A) \to j \in ℤ$
60		eluzelz	$⊢ K (N) \in ℤ_{\geq M} \to K (N) \in ℤ$
61	28 60	syl	$⊢ φ \to K (N) \in ℤ$
62	61	adantr	$⊢ (φ \land j \in A) \to K (N) \in ℤ$
63		eluz	$⊢ (j \in ℤ \land K (N) \in ℤ) \to (K (N) \in ℤ_{\geq j} \leftrightarrow j \leq K (N))$
64	59 62 63	syl2anc	$⊢ (φ \land j \in A) \to (K (N) \in ℤ_{\geq j} \leftrightarrow j \leq K (N))$
65	57 64	mpbird	$⊢ (φ \land j \in A) \to K (N) \in ℤ_{\geq j}$
66		elfzuzb	$⊢ j \in (M \dots K (N)) \leftrightarrow (j \in ℤ_{\geq M} \land K (N) \in ℤ_{\geq j})$
67	29 65 66	sylanbrc	$⊢ (φ \land j \in A) \to j \in (M \dots K (N))$
68	67	ex	$⊢ φ \to (j \in A \to j \in (M \dots K (N)))$
69	68	ssrdv	$⊢ φ \to A \subseteq (M \dots K (N))$
70	1 2 28 69	fprodcvg	$⊢ φ \to seq M (\times F) ⇝ seq M (\times F) (K (N))$
71		mullid	$⊢ m \in ℂ \to 1 m = m$
72	71	adantl	$⊢ (φ \land m \in ℂ) \to 1 m = m$
73		mulrid	$⊢ m \in ℂ \to m \cdot 1 = m$
74	73	adantl	$⊢ (φ \land m \in ℂ) \to m \cdot 1 = m$
75		mulcl	$⊢ (m \in ℂ \land x \in ℂ) \to m x \in ℂ$
76	75	adantl	$⊢ (φ \land (m \in ℂ \land x \in ℂ)) \to m x \in ℂ$
77		1cnd	$⊢ φ \to 1 \in ℂ$
78	26 16	eleqtrrd	$⊢ φ \to N \in (1 \dots \|A\|)$
79		iftrue	$⊢ k \in A \to if (k \in A, B, 1) = B$
80	79	adantl	$⊢ (φ \land k \in A) \to if (k \in A, B, 1) = B$
81	80 2	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, B, 1) \in ℂ$
82	81	ex	$⊢ φ \to (k \in A \to if (k \in A, B, 1) \in ℂ)$
83		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 1) = 1$
84		ax-1cn	$⊢ 1 \in ℂ$
85	83 84	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 1) \in ℂ$
86	82 85	pm2.61d1	$⊢ φ \to if (k \in A, B, 1) \in ℂ$
87	86	adantr	$⊢ (φ \land k \in ℤ) \to if (k \in A, B, 1) \in ℂ$
88	87 1	fmptd	$⊢ φ \to F : ℤ ⟶ ℂ$
89		elfzelz	$⊢ m \in (M \dots K (\|A\|)) \to m \in ℤ$
90		ffvelcdm	$⊢ (F : ℤ ⟶ ℂ \land m \in ℤ) \to F (m) \in ℂ$
91	88 89 90	syl2an	$⊢ (φ \land m \in (M \dots K (\|A\|))) \to F (m) \in ℂ$
92		fveqeq2	$⊢ k = m \to (F (k) = 1 \leftrightarrow F (m) = 1)$
93		eldifi	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to k \in (M \dots K (\|A\|))$
94	93	elfzelzd	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to k \in ℤ$
95		eldifn	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to \neg k \in A$
96	95 83	syl	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to if (k \in A, B, 1) = 1$
97	96 84	eqeltrdi	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to if (k \in A, B, 1) \in ℂ$
98	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 1) \in ℂ) \to F (k) = if (k \in A, B, 1)$
99	94 97 98	syl2anc	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to F (k) = if (k \in A, B, 1)$
100	99 96	eqtrd	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to F (k) = 1$
101	92 100	vtoclga	$⊢ m \in ((M \dots K (\|A\|)) ∖ A) \to F (m) = 1$
102	101	adantl	$⊢ (φ \land m \in ((M \dots K (\|A\|)) ∖ A)) \to F (m) = 1$
103		isof1o	$⊢ K {Isom}_{<, <} ((1 \dots \|A\|), A) \to K : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
104		f1of	$⊢ K : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to K : (1 \dots \|A\|) ⟶ A$
105	9 103 104	3syl	$⊢ φ \to K : (1 \dots \|A\|) ⟶ A$
106	105	ffvelcdmda	$⊢ (φ \land x \in (1 \dots \|A\|)) \to K (x) \in A$
107	106	iftrued	$⊢ (φ \land x \in (1 \dots \|A\|)) \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) = ⦋ K (x) / k ⦌ B$
108	58	adantr	$⊢ (φ \land x \in (1 \dots \|A\|)) \to A \subseteq ℤ$
109	108 106	sseldd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to K (x) \in ℤ$
110		nfv	$⊢ Ⅎ k φ$
111		nfv	$⊢ Ⅎ k K (x) \in A$
112		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ K (x) / k ⦌ B$
113		nfcv	$⊢ \underline{Ⅎ} k 1$
114	111 112 113	nfif	$⊢ \underline{Ⅎ} k if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1)$
115	114	nfel1	$⊢ Ⅎ k if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ$
116	110 115	nfim	$⊢ Ⅎ k (φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ)$
117		fvex	$⊢ K (x) \in V$
118		eleq1	$⊢ k = K (x) \to (k \in A \leftrightarrow K (x) \in A)$
119		csbeq1a	$⊢ k = K (x) \to B = ⦋ K (x) / k ⦌ B$
120	118 119	ifbieq1d	$⊢ k = K (x) \to if (k \in A, B, 1) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1)$
121	120	eleq1d	$⊢ k = K (x) \to (if (k \in A, B, 1) \in ℂ \leftrightarrow if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ)$
122	121	imbi2d	$⊢ k = K (x) \to ((φ \to if (k \in A, B, 1) \in ℂ) \leftrightarrow (φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ))$
123	116 117 122 86	vtoclf	$⊢ φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ$
124	123	adantr	$⊢ (φ \land x \in (1 \dots \|A\|)) \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ$
125		eleq1	$⊢ n = K (x) \to (n \in A \leftrightarrow K (x) \in A)$
126		csbeq1	$⊢ n = K (x) \to ⦋ n / k ⦌ B = ⦋ K (x) / k ⦌ B$
127	125 126	ifbieq1d	$⊢ n = K (x) \to if (n \in A, ⦋ n / k ⦌ B, 1) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1)$
128		nfcv	$⊢ \underline{Ⅎ} n if (k \in A, B, 1)$
129		nfv	$⊢ Ⅎ k n \in A$
130		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
131	129 130 113	nfif	$⊢ \underline{Ⅎ} k if (n \in A, ⦋ n / k ⦌ B, 1)$
132		eleq1	$⊢ k = n \to (k \in A \leftrightarrow n \in A)$
133		csbeq1a	$⊢ k = n \to B = ⦋ n / k ⦌ B$
134	132 133	ifbieq1d	$⊢ k = n \to if (k \in A, B, 1) = if (n \in A, ⦋ n / k ⦌ B, 1)$
135	128 131 134	cbvmpt	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 1))$
136	1 135	eqtri	$⊢ F = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 1))$
137	127 136	fvmptg	$⊢ (K (x) \in ℤ \land if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1) \in ℂ) \to F (K (x)) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1)$
138	109 124 137	syl2anc	$⊢ (φ \land x \in (1 \dots \|A\|)) \to F (K (x)) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 1)$
139		elfznn	$⊢ x \in (1 \dots \|A\|) \to x \in ℕ$
140	107 124	eqeltrrd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to ⦋ K (x) / k ⦌ B \in ℂ$
141		fveq2	$⊢ j = x \to K (j) = K (x)$
142	141	csbeq1d	$⊢ j = x \to ⦋ K (j) / k ⦌ B = ⦋ K (x) / k ⦌ B$
143	142 4	fvmptg	$⊢ (x \in ℕ \land ⦋ K (x) / k ⦌ B \in ℂ) \to H (x) = ⦋ K (x) / k ⦌ B$
144	139 140 143	syl2an2	$⊢ (φ \land x \in (1 \dots \|A\|)) \to H (x) = ⦋ K (x) / k ⦌ B$
145	107 138 144	3eqtr4rd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to H (x) = F (K (x))$
146	72 74 76 77 9 78 7 91 102 145	seqcoll	$⊢ φ \to seq M (\times F) (K (N)) = seq 1 (\times H) (N)$
147	5 5	jca	$⊢ φ \to (N \in ℕ \land N \in ℕ)$
148	1 2 3 4 147 8 30	prodmolem3	$⊢ φ \to seq 1 (\times G) (N) = seq 1 (\times H) (N)$
149	146 148	eqtr4d	$⊢ φ \to seq M (\times F) (K (N)) = seq 1 (\times G) (N)$
150	70 149	breqtrd	$⊢ φ \to seq M (\times F) ⇝ seq 1 (\times G) (N)$

Metamath Proof Explorer

Theorem prodmolem2a

Proof