summolem2a

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

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		summo.3	$⊢ G = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
4		summolem2.4	$⊢ H = (n \in ℕ ⟼ ⦋ K (n) / k ⦌ B)$
5		summolem2.5	$⊢ φ \to N \in ℕ$
6		summolem2.6	$⊢ φ \to M \in ℤ$
7		summolem2.7	$⊢ φ \to A \subseteq ℤ_{\geq M}$
8		summolem2.8	$⊢ φ \to f : (1 \dots N) \underset{1-1 onto}{⟶} A$
9		summolem2.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		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
13		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
14	5 12 13	3syl	$⊢ φ \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	19 20	syl	$⊢ φ \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
22		f1of	$⊢ K : (1 \dots N) \underset{1-1 onto}{⟶} A \to K : (1 \dots N) ⟶ A$
23	21 22	syl	$⊢ φ \to K : (1 \dots N) ⟶ A$
24		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
25	5 24	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
26		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
27	25 26	syl	$⊢ φ \to N \in (1 \dots N)$
28	23 27	ffvelrnd	$⊢ φ \to K (N) \in A$
29	7 28	sseldd	$⊢ φ \to K (N) \in ℤ_{\geq M}$
30	7	sselda	$⊢ (φ \land n \in A) \to n \in ℤ_{\geq M}$
31		f1ocnvfv2	$⊢ (K : (1 \dots N) \underset{1-1 onto}{⟶} A \land n \in A) \to K (K^{-1} (n)) = n$
32	21 31	sylan	$⊢ (φ \land n \in A) \to K (K^{-1} (n)) = n$
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	21 33 34	3syl	$⊢ φ \to K^{-1} : A ⟶ (1 \dots N)$
36	35	ffvelrnda	$⊢ (φ \land n \in A) \to K^{-1} (n) \in (1 \dots N)$
37		elfzle2	$⊢ K^{-1} (n) \in (1 \dots N) \to K^{-1} (n) \leq N$
38	36 37	syl	$⊢ (φ \land n \in A) \to K^{-1} (n) \leq N$
39	19	adantr	$⊢ (φ \land n \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 n \in A) \to (1 \dots N) \subseteq ℝ^{*}$
48	7	adantr	$⊢ (φ \land n \in A) \to A \subseteq ℤ_{\geq M}$
49		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
50	49 42	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
51	48 50	sstrdi	$⊢ (φ \land n \in A) \to A \subseteq ℝ$
52	51 45	sstrdi	$⊢ (φ \land n \in A) \to A \subseteq ℝ^{*}$
53	27	adantr	$⊢ (φ \land n \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} (n) \in (1 \dots N) \land N \in (1 \dots N))) \to (K^{-1} (n) \leq N \leftrightarrow K (K^{-1} (n)) \leq K (N))$
55	39 47 52 36 53 54	syl122anc	$⊢ (φ \land n \in A) \to (K^{-1} (n) \leq N \leftrightarrow K (K^{-1} (n)) \leq K (N))$
56	38 55	mpbid	$⊢ (φ \land n \in A) \to K (K^{-1} (n)) \leq K (N)$
57	32 56	eqbrtrrd	$⊢ (φ \land n \in A) \to n \leq K (N)$
58		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
59	30 58	syl	$⊢ (φ \land n \in A) \to n \in ℤ$
60		eluzelz	$⊢ K (N) \in ℤ_{\geq M} \to K (N) \in ℤ$
61	29 60	syl	$⊢ φ \to K (N) \in ℤ$
62	61	adantr	$⊢ (φ \land n \in A) \to K (N) \in ℤ$
63		eluz	$⊢ (n \in ℤ \land K (N) \in ℤ) \to (K (N) \in ℤ_{\geq n} \leftrightarrow n \leq K (N))$
64	59 62 63	syl2anc	$⊢ (φ \land n \in A) \to (K (N) \in ℤ_{\geq n} \leftrightarrow n \leq K (N))$
65	57 64	mpbird	$⊢ (φ \land n \in A) \to K (N) \in ℤ_{\geq n}$
66		elfzuzb	$⊢ n \in (M \dots K (N)) \leftrightarrow (n \in ℤ_{\geq M} \land K (N) \in ℤ_{\geq n})$
67	30 65 66	sylanbrc	$⊢ (φ \land n \in A) \to n \in (M \dots K (N))$
68	67	ex	$⊢ φ \to (n \in A \to n \in (M \dots K (N)))$
69	68	ssrdv	$⊢ φ \to A \subseteq (M \dots K (N))$
70	1 2 29 69	fsumcvg	$⊢ φ \to seq M (+ F) ⇝ seq M (+ F) (K (N))$
71		addid2	$⊢ m \in ℂ \to 0 + m = m$
72	71	adantl	$⊢ (φ \land m \in ℂ) \to 0 + m = m$
73		addid1	$⊢ m \in ℂ \to m + 0 = m$
74	73	adantl	$⊢ (φ \land m \in ℂ) \to m + 0 = m$
75		addcl	$⊢ (m \in ℂ \land x \in ℂ) \to m + x \in ℂ$
76	75	adantl	$⊢ (φ \land (m \in ℂ \land x \in ℂ)) \to m + x \in ℂ$
77		0cnd	$⊢ φ \to 0 \in ℂ$
78	27 16	eleqtrrd	$⊢ φ \to N \in (1 \dots \|A\|)$
79		iftrue	$⊢ k \in A \to if (k \in A, B, 0) = B$
80	79	adantl	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) = B$
81	80 2	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) \in ℂ$
82	81	ex	$⊢ φ \to (k \in A \to if (k \in A, B, 0) \in ℂ)$
83		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 0) = 0$
84		0cn	$⊢ 0 \in ℂ$
85	83 84	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 0) \in ℂ$
86	82 85	pm2.61d1	$⊢ φ \to if (k \in A, B, 0) \in ℂ$
87	86	adantr	$⊢ (φ \land k \in ℤ) \to if (k \in A, B, 0) \in ℂ$
88	87 1	fmptd	$⊢ φ \to F : ℤ ⟶ ℂ$
89		elfzelz	$⊢ m \in (M \dots K (\|A\|)) \to m \in ℤ$
90		ffvelrn	$⊢ (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) = 0 \leftrightarrow F (m) = 0)$
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, 0) = 0$
97	96 84	eqeltrdi	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to if (k \in A, B, 0) \in ℂ$
98	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 0) \in ℂ) \to F (k) = if (k \in A, B, 0)$
99	94 97 98	syl2anc	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to F (k) = if (k \in A, B, 0)$
100	99 96	eqtrd	$⊢ k \in ((M \dots K (\|A\|)) ∖ A) \to F (k) = 0$
101	92 100	vtoclga	$⊢ m \in ((M \dots K (\|A\|)) ∖ A) \to F (m) = 0$
102	101	adantl	$⊢ (φ \land m \in ((M \dots K (\|A\|)) ∖ A)) \to F (m) = 0$
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	ffvelrnda	$⊢ (φ \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, 0) = ⦋ K (x) / k ⦌ B$
108	7	adantr	$⊢ (φ \land x \in (1 \dots \|A\|)) \to A \subseteq ℤ_{\geq M}$
109	108 106	sseldd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to K (x) \in ℤ_{\geq M}$
110		eluzelz	$⊢ K (x) \in ℤ_{\geq M} \to K (x) \in ℤ$
111	109 110	syl	$⊢ (φ \land x \in (1 \dots \|A\|)) \to K (x) \in ℤ$
112		nfv	$⊢ Ⅎ k φ$
113		nfv	$⊢ Ⅎ k K (x) \in A$
114		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ K (x) / k ⦌ B$
115		nfcv	$⊢ \underline{Ⅎ} k 0$
116	113 114 115	nfif	$⊢ \underline{Ⅎ} k if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0)$
117	116	nfel1	$⊢ Ⅎ k if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ$
118	112 117	nfim	$⊢ Ⅎ k (φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ)$
119		fvex	$⊢ K (x) \in V$
120		eleq1	$⊢ k = K (x) \to (k \in A \leftrightarrow K (x) \in A)$
121		csbeq1a	$⊢ k = K (x) \to B = ⦋ K (x) / k ⦌ B$
122	120 121	ifbieq1d	$⊢ k = K (x) \to if (k \in A, B, 0) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0)$
123	122	eleq1d	$⊢ k = K (x) \to (if (k \in A, B, 0) \in ℂ \leftrightarrow if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ)$
124	123	imbi2d	$⊢ k = K (x) \to ((φ \to if (k \in A, B, 0) \in ℂ) \leftrightarrow (φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ))$
125	118 119 124 86	vtoclf	$⊢ φ \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ$
126	125	adantr	$⊢ (φ \land x \in (1 \dots \|A\|)) \to if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ$
127		eleq1	$⊢ n = K (x) \to (n \in A \leftrightarrow K (x) \in A)$
128		csbeq1	$⊢ n = K (x) \to ⦋ n / k ⦌ B = ⦋ K (x) / k ⦌ B$
129	127 128	ifbieq1d	$⊢ n = K (x) \to if (n \in A, ⦋ n / k ⦌ B, 0) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0)$
130		nfcv	$⊢ \underline{Ⅎ} n if (k \in A, B, 0)$
131		nfv	$⊢ Ⅎ k n \in A$
132		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
133	131 132 115	nfif	$⊢ \underline{Ⅎ} k if (n \in A, ⦋ n / k ⦌ B, 0)$
134		eleq1	$⊢ k = n \to (k \in A \leftrightarrow n \in A)$
135		csbeq1a	$⊢ k = n \to B = ⦋ n / k ⦌ B$
136	134 135	ifbieq1d	$⊢ k = n \to if (k \in A, B, 0) = if (n \in A, ⦋ n / k ⦌ B, 0)$
137	130 133 136	cbvmpt	$⊢ (k \in ℤ ⟼ if (k \in A, B, 0)) = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))$
138	1 137	eqtri	$⊢ F = (n \in ℤ ⟼ if (n \in A, ⦋ n / k ⦌ B, 0))$
139	129 138	fvmptg	$⊢ (K (x) \in ℤ \land if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0) \in ℂ) \to F (K (x)) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0)$
140	111 126 139	syl2anc	$⊢ (φ \land x \in (1 \dots \|A\|)) \to F (K (x)) = if (K (x) \in A, ⦋ K (x) / k ⦌ B, 0)$
141		elfznn	$⊢ x \in (1 \dots \|A\|) \to x \in ℕ$
142	107 126	eqeltrrd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to ⦋ K (x) / k ⦌ B \in ℂ$
143		fveq2	$⊢ n = x \to K (n) = K (x)$
144	143	csbeq1d	$⊢ n = x \to ⦋ K (n) / k ⦌ B = ⦋ K (x) / k ⦌ B$
145	144 4	fvmptg	$⊢ (x \in ℕ \land ⦋ K (x) / k ⦌ B \in ℂ) \to H (x) = ⦋ K (x) / k ⦌ B$
146	141 142 145	syl2an2	$⊢ (φ \land x \in (1 \dots \|A\|)) \to H (x) = ⦋ K (x) / k ⦌ B$
147	107 140 146	3eqtr4rd	$⊢ (φ \land x \in (1 \dots \|A\|)) \to H (x) = F (K (x))$
148	72 74 76 77 9 78 7 91 102 147	seqcoll	$⊢ φ \to seq M (+ F) (K (N)) = seq 1 (+ H) (N)$
149	5 5	jca	$⊢ φ \to (N \in ℕ \land N \in ℕ)$
150	1 2 3 4 149 8 21	summolem3	$⊢ φ \to seq 1 (+ G) (N) = seq 1 (+ H) (N)$
151	148 150	eqtr4d	$⊢ φ \to seq M (+ F) (K (N)) = seq 1 (+ G) (N)$
152	70 151	breqtrd	$⊢ φ \to seq M (+ F) ⇝ seq 1 (+ G) (N)$

Metamath Proof Explorer

Theorem summolem2a

Proof