Metamath Proof Explorer


Theorem dvnprodlem1

Description: D is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnprodlem1.c C = s 𝒫 T n 0 c 0 n s | t s c t = n
dvnprodlem1.j φ J 0
dvnprodlem1.d D = c C R Z J J c Z c R
dvnprodlem1.t φ T Fin
dvnprodlem1.z φ Z T
dvnprodlem1.zr φ ¬ Z R
dvnprodlem1.rzt φ R Z T
Assertion dvnprodlem1 φ D : C R Z J 1-1 onto k = 0 J k × C R k

Proof

Step Hyp Ref Expression
1 dvnprodlem1.c C = s 𝒫 T n 0 c 0 n s | t s c t = n
2 dvnprodlem1.j φ J 0
3 dvnprodlem1.d D = c C R Z J J c Z c R
4 dvnprodlem1.t φ T Fin
5 dvnprodlem1.z φ Z T
6 dvnprodlem1.zr φ ¬ Z R
7 dvnprodlem1.rzt φ R Z T
8 eqidd φ c C R Z J J c Z c R = J c Z c R
9 0zd φ c C R Z J 0
10 2 nn0zd φ J
11 10 adantr φ c C R Z J J
12 oveq2 s = R Z 0 n s = 0 n R Z
13 rabeq 0 n s = 0 n R Z c 0 n s | t s c t = n = c 0 n R Z | t s c t = n
14 12 13 syl s = R Z c 0 n s | t s c t = n = c 0 n R Z | t s c t = n
15 sumeq1 s = R Z t s c t = t R Z c t
16 15 eqeq1d s = R Z t s c t = n t R Z c t = n
17 16 rabbidv s = R Z c 0 n R Z | t s c t = n = c 0 n R Z | t R Z c t = n
18 14 17 eqtrd s = R Z c 0 n s | t s c t = n = c 0 n R Z | t R Z c t = n
19 18 mpteq2dv s = R Z n 0 c 0 n s | t s c t = n = n 0 c 0 n R Z | t R Z c t = n
20 ssexg R Z T T Fin R Z V
21 7 4 20 syl2anc φ R Z V
22 elpwg R Z V R Z 𝒫 T R Z T
23 21 22 syl φ R Z 𝒫 T R Z T
24 7 23 mpbird φ R Z 𝒫 T
25 nn0ex 0 V
26 25 mptex n 0 c 0 n R Z | t R Z c t = n V
27 26 a1i φ n 0 c 0 n R Z | t R Z c t = n V
28 1 19 24 27 fvmptd3 φ C R Z = n 0 c 0 n R Z | t R Z c t = n
29 oveq2 n = J 0 n = 0 J
30 29 oveq1d n = J 0 n R Z = 0 J R Z
31 rabeq 0 n R Z = 0 J R Z c 0 n R Z | t R Z c t = n = c 0 J R Z | t R Z c t = n
32 30 31 syl n = J c 0 n R Z | t R Z c t = n = c 0 J R Z | t R Z c t = n
33 eqeq2 n = J t R Z c t = n t R Z c t = J
34 33 rabbidv n = J c 0 J R Z | t R Z c t = n = c 0 J R Z | t R Z c t = J
35 32 34 eqtrd n = J c 0 n R Z | t R Z c t = n = c 0 J R Z | t R Z c t = J
36 35 adantl φ n = J c 0 n R Z | t R Z c t = n = c 0 J R Z | t R Z c t = J
37 ovex 0 J R Z V
38 37 rabex c 0 J R Z | t R Z c t = J V
39 38 a1i φ c 0 J R Z | t R Z c t = J V
40 28 36 2 39 fvmptd φ C R Z J = c 0 J R Z | t R Z c t = J
41 ssrab2 c 0 J R Z | t R Z c t = J 0 J R Z
42 41 a1i φ c 0 J R Z | t R Z c t = J 0 J R Z
43 40 42 eqsstrd φ C R Z J 0 J R Z
44 43 adantr φ c C R Z J C R Z J 0 J R Z
45 simpr φ c C R Z J c C R Z J
46 44 45 sseldd φ c C R Z J c 0 J R Z
47 elmapi c 0 J R Z c : R Z 0 J
48 46 47 syl φ c C R Z J c : R Z 0 J
49 snidg Z T Z Z
50 5 49 syl φ Z Z
51 elun2 Z Z Z R Z
52 50 51 syl φ Z R Z
53 52 adantr φ c C R Z J Z R Z
54 48 53 ffvelrnd φ c C R Z J c Z 0 J
55 54 elfzelzd φ c C R Z J c Z
56 11 55 zsubcld φ c C R Z J J c Z
57 elfzle2 c Z 0 J c Z J
58 54 57 syl φ c C R Z J c Z J
59 11 zred φ c C R Z J J
60 55 zred φ c C R Z J c Z
61 59 60 subge0d φ c C R Z J 0 J c Z c Z J
62 58 61 mpbird φ c C R Z J 0 J c Z
63 elfzle1 c Z 0 J 0 c Z
64 54 63 syl φ c C R Z J 0 c Z
65 59 60 subge02d φ c C R Z J 0 c Z J c Z J
66 64 65 mpbid φ c C R Z J J c Z J
67 9 11 56 62 66 elfzd φ c C R Z J J c Z 0 J
68 elmapfn c 0 J R Z c Fn R Z
69 46 68 syl φ c C R Z J c Fn R Z
70 ssun1 R R Z
71 70 a1i φ c C R Z J R R Z
72 fnssres c Fn R Z R R Z c R Fn R
73 69 71 72 syl2anc φ c C R Z J c R Fn R
74 nfv t φ
75 nfcv _ t c
76 nfcv _ t 𝒫 T
77 nfcv _ t 0
78 nfcv _ t s
79 78 nfsum1 _ t t s c t
80 nfcv _ t n
81 79 80 nfeq t t s c t = n
82 nfcv _ t 0 n s
83 81 82 nfrabw _ t c 0 n s | t s c t = n
84 77 83 nfmpt _ t n 0 c 0 n s | t s c t = n
85 76 84 nfmpt _ t s 𝒫 T n 0 c 0 n s | t s c t = n
86 1 85 nfcxfr _ t C
87 nfcv _ t R Z
88 86 87 nffv _ t C R Z
89 nfcv _ t J
90 88 89 nffv _ t C R Z J
91 75 90 nfel t c C R Z J
92 74 91 nfan t φ c C R Z J
93 fvres t R c R t = c t
94 93 adantl φ c C R Z J t R c R t = c t
95 9 adantr φ c C R Z J t R 0
96 56 adantr φ c C R Z J t R J c Z
97 48 adantr φ c C R Z J t R c : R Z 0 J
98 71 sselda φ c C R Z J t R t R Z
99 97 98 ffvelrnd φ c C R Z J t R c t 0 J
100 99 elfzelzd φ c C R Z J t R c t
101 elfzle1 c t 0 J 0 c t
102 99 101 syl φ c C R Z J t R 0 c t
103 7 unssad φ R T
104 ssfi T Fin R T R Fin
105 4 103 104 syl2anc φ R Fin
106 105 ad2antrr φ c C R Z J t R R Fin
107 fzssz 0 J
108 zssre
109 107 108 sstri 0 J
110 109 a1i φ c C R Z J r R 0 J
111 48 adantr φ c C R Z J r R c : R Z 0 J
112 71 sselda φ c C R Z J r R r R Z
113 111 112 ffvelrnd φ c C R Z J r R c r 0 J
114 110 113 sseldd φ c C R Z J r R c r
115 114 adantlr φ c C R Z J t R r R c r
116 elfzle1 c r 0 J 0 c r
117 113 116 syl φ c C R Z J r R 0 c r
118 117 adantlr φ c C R Z J t R r R 0 c r
119 fveq2 r = t c r = c t
120 simpr φ c C R Z J t R t R
121 106 115 118 119 120 fsumge1 φ c C R Z J t R c t r R c r
122 105 adantr φ c C R Z J R Fin
123 114 recnd φ c C R Z J r R c r
124 122 123 fsumcl φ c C R Z J r R c r
125 60 recnd φ c C R Z J c Z
126 124 125 pncand φ c C R Z J r R c r + c Z - c Z = r R c r
127 nfv r φ c C R Z J
128 nfcv _ r c Z
129 5 adantr φ c C R Z J Z T
130 6 adantr φ c C R Z J ¬ Z R
131 fveq2 r = Z c r = c Z
132 127 128 122 129 130 123 131 125 fsumsplitsn φ c C R Z J r R Z c r = r R c r + c Z
133 132 eqcomd φ c C R Z J r R c r + c Z = r R Z c r
134 119 cbvsumv r R Z c r = t R Z c t
135 134 a1i φ c C R Z J r R Z c r = t R Z c t
136 40 adantr φ c C R Z J C R Z J = c 0 J R Z | t R Z c t = J
137 45 136 eleqtrd φ c C R Z J c c 0 J R Z | t R Z c t = J
138 rabid c c 0 J R Z | t R Z c t = J c 0 J R Z t R Z c t = J
139 137 138 sylib φ c C R Z J c 0 J R Z t R Z c t = J
140 139 simprd φ c C R Z J t R Z c t = J
141 135 140 eqtrd φ c C R Z J r R Z c r = J
142 133 141 eqtrd φ c C R Z J r R c r + c Z = J
143 142 oveq1d φ c C R Z J r R c r + c Z - c Z = J c Z
144 126 143 eqtr3d φ c C R Z J r R c r = J c Z
145 144 adantr φ c C R Z J t R r R c r = J c Z
146 121 145 breqtrd φ c C R Z J t R c t J c Z
147 95 96 100 102 146 elfzd φ c C R Z J t R c t 0 J c Z
148 94 147 eqeltrd φ c C R Z J t R c R t 0 J c Z
149 148 ex φ c C R Z J t R c R t 0 J c Z
150 92 149 ralrimi φ c C R Z J t R c R t 0 J c Z
151 73 150 jca φ c C R Z J c R Fn R t R c R t 0 J c Z
152 ffnfv c R : R 0 J c Z c R Fn R t R c R t 0 J c Z
153 151 152 sylibr φ c C R Z J c R : R 0 J c Z
154 ovexd φ c C R Z J 0 J c Z V
155 4 103 ssexd φ R V
156 155 adantr φ c C R Z J R V
157 154 156 elmapd φ c C R Z J c R 0 J c Z R c R : R 0 J c Z
158 153 157 mpbird φ c C R Z J c R 0 J c Z R
159 93 a1i φ c C R Z J t R c R t = c t
160 92 159 ralrimi φ c C R Z J t R c R t = c t
161 160 sumeq2d φ c C R Z J t R c R t = t R c t
162 119 cbvsumv r R c r = t R c t
163 162 eqcomi t R c t = r R c r
164 163 a1i φ c C R Z J t R c t = r R c r
165 144 idi φ c C R Z J r R c r = J c Z
166 161 164 165 3eqtrd φ c C R Z J t R c R t = J c Z
167 158 166 jca φ c C R Z J c R 0 J c Z R t R c R t = J c Z
168 eqidd e = c R R = R
169 simpl e = c R t R e = c R
170 169 fveq1d e = c R t R e t = c R t
171 168 170 sumeq12rdv e = c R t R e t = t R c R t
172 171 eqeq1d e = c R t R e t = J c Z t R c R t = J c Z
173 172 elrab c R e 0 J c Z R | t R e t = J c Z c R 0 J c Z R t R c R t = J c Z
174 167 173 sylibr φ c C R Z J c R e 0 J c Z R | t R e t = J c Z
175 oveq2 s = R 0 n s = 0 n R
176 rabeq 0 n s = 0 n R c 0 n s | t s c t = n = c 0 n R | t s c t = n
177 175 176 syl s = R c 0 n s | t s c t = n = c 0 n R | t s c t = n
178 sumeq1 s = R t s c t = t R c t
179 178 eqeq1d s = R t s c t = n t R c t = n
180 179 rabbidv s = R c 0 n R | t s c t = n = c 0 n R | t R c t = n
181 177 180 eqtrd s = R c 0 n s | t s c t = n = c 0 n R | t R c t = n
182 181 mpteq2dv s = R n 0 c 0 n s | t s c t = n = n 0 c 0 n R | t R c t = n
183 elpwg R V R 𝒫 T R T
184 155 183 syl φ R 𝒫 T R T
185 103 184 mpbird φ R 𝒫 T
186 25 mptex n 0 c 0 n R | t R c t = n V
187 186 a1i φ n 0 c 0 n R | t R c t = n V
188 1 182 185 187 fvmptd3 φ C R = n 0 c 0 n R | t R c t = n
189 188 adantr φ c C R Z J C R = n 0 c 0 n R | t R c t = n
190 oveq2 n = m 0 n = 0 m
191 190 oveq1d n = m 0 n R = 0 m R
192 rabeq 0 n R = 0 m R c 0 n R | t R c t = n = c 0 m R | t R c t = n
193 191 192 syl n = m c 0 n R | t R c t = n = c 0 m R | t R c t = n
194 eqeq2 n = m t R c t = n t R c t = m
195 194 rabbidv n = m c 0 m R | t R c t = n = c 0 m R | t R c t = m
196 193 195 eqtrd n = m c 0 n R | t R c t = n = c 0 m R | t R c t = m
197 196 cbvmptv n 0 c 0 n R | t R c t = n = m 0 c 0 m R | t R c t = m
198 197 a1i φ c C R Z J n 0 c 0 n R | t R c t = n = m 0 c 0 m R | t R c t = m
199 189 198 eqtrd φ c C R Z J C R = m 0 c 0 m R | t R c t = m
200 fveq1 c = e c t = e t
201 200 sumeq2sdv c = e t R c t = t R e t
202 201 eqeq1d c = e t R c t = m t R e t = m
203 202 cbvrabv c 0 m R | t R c t = m = e 0 m R | t R e t = m
204 203 a1i m = J c Z c 0 m R | t R c t = m = e 0 m R | t R e t = m
205 oveq2 m = J c Z 0 m = 0 J c Z
206 205 oveq1d m = J c Z 0 m R = 0 J c Z R
207 rabeq 0 m R = 0 J c Z R e 0 m R | t R e t = m = e 0 J c Z R | t R e t = m
208 206 207 syl m = J c Z e 0 m R | t R e t = m = e 0 J c Z R | t R e t = m
209 eqeq2 m = J c Z t R e t = m t R e t = J c Z
210 209 rabbidv m = J c Z e 0 J c Z R | t R e t = m = e 0 J c Z R | t R e t = J c Z
211 204 208 210 3eqtrd m = J c Z c 0 m R | t R c t = m = e 0 J c Z R | t R e t = J c Z
212 211 adantl φ c C R Z J m = J c Z c 0 m R | t R c t = m = e 0 J c Z R | t R e t = J c Z
213 56 62 jca φ c C R Z J J c Z 0 J c Z
214 elnn0z J c Z 0 J c Z 0 J c Z
215 213 214 sylibr φ c C R Z J J c Z 0
216 ovex 0 J c Z R V
217 216 rabex e 0 J c Z R | t R e t = J c Z V
218 217 a1i φ c C R Z J e 0 J c Z R | t R e t = J c Z V
219 199 212 215 218 fvmptd φ c C R Z J C R J c Z = e 0 J c Z R | t R e t = J c Z
220 219 eqcomd φ c C R Z J e 0 J c Z R | t R e t = J c Z = C R J c Z
221 174 220 eleqtrd φ c C R Z J c R C R J c Z
222 67 221 jca φ c C R Z J J c Z 0 J c R C R J c Z
223 8 222 jca φ c C R Z J J c Z c R = J c Z c R J c Z 0 J c R C R J c Z
224 ovexd φ c C R Z J J c Z V
225 vex c V
226 225 resex c R V
227 226 a1i φ c C R Z J c R V
228 opeq12 k = J c Z d = c R k d = J c Z c R
229 228 eqeq2d k = J c Z d = c R J c Z c R = k d J c Z c R = J c Z c R
230 eleq1 k = J c Z k 0 J J c Z 0 J
231 230 adantr k = J c Z d = c R k 0 J J c Z 0 J
232 simpr k = J c Z d = c R d = c R
233 fveq2 k = J c Z C R k = C R J c Z
234 233 adantr k = J c Z d = c R C R k = C R J c Z
235 232 234 eleq12d k = J c Z d = c R d C R k c R C R J c Z
236 231 235 anbi12d k = J c Z d = c R k 0 J d C R k J c Z 0 J c R C R J c Z
237 229 236 anbi12d k = J c Z d = c R J c Z c R = k d k 0 J d C R k J c Z c R = J c Z c R J c Z 0 J c R C R J c Z
238 237 spc2egv J c Z V c R V J c Z c R = J c Z c R J c Z 0 J c R C R J c Z k d J c Z c R = k d k 0 J d C R k
239 224 227 238 syl2anc φ c C R Z J J c Z c R = J c Z c R J c Z 0 J c R C R J c Z k d J c Z c R = k d k 0 J d C R k
240 223 239 mpd φ c C R Z J k d J c Z c R = k d k 0 J d C R k
241 eliunxp J c Z c R k = 0 J k × C R k k d J c Z c R = k d k 0 J d C R k
242 240 241 sylibr φ c C R Z J J c Z c R k = 0 J k × C R k
243 242 3 fmptd φ D : C R Z J k = 0 J k × C R k
244 90 nfcri t e C R Z J
245 91 244 nfan t c C R Z J e C R Z J
246 74 245 nfan t φ c C R Z J e C R Z J
247 nfv t D c = D e
248 246 247 nfan t φ c C R Z J e C R Z J D c = D e
249 94 eqcomd φ c C R Z J t R c t = c R t
250 249 adantlrr φ c C R Z J e C R Z J t R c t = c R t
251 250 adantlr φ c C R Z J e C R Z J D c = D e t R c t = c R t
252 3 a1i φ D = c C R Z J J c Z c R
253 opex J c Z c R V
254 253 a1i φ c C R Z J J c Z c R V
255 252 254 fvmpt2d φ c C R Z J D c = J c Z c R
256 255 fveq2d φ c C R Z J 2 nd D c = 2 nd J c Z c R
257 256 fveq1d φ c C R Z J 2 nd D c t = 2 nd J c Z c R t
258 ovex J c Z V
259 258 226 op2nd 2 nd J c Z c R = c R
260 259 fveq1i 2 nd J c Z c R t = c R t
261 260 a1i φ c C R Z J 2 nd J c Z c R t = c R t
262 257 261 eqtr2d φ c C R Z J c R t = 2 nd D c t
263 262 adantrr φ c C R Z J e C R Z J c R t = 2 nd D c t
264 263 ad2antrr φ c C R Z J e C R Z J D c = D e t R c R t = 2 nd D c t
265 simpr φ e C R Z J D c = D e D c = D e
266 fveq1 c = e c Z = e Z
267 266 oveq2d c = e J c Z = J e Z
268 reseq1 c = e c R = e R
269 267 268 opeq12d c = e J c Z c R = J e Z e R
270 simpr φ e C R Z J e C R Z J
271 opex J e Z e R V
272 271 a1i φ e C R Z J J e Z e R V
273 3 269 270 272 fvmptd3 φ e C R Z J D e = J e Z e R
274 273 adantr φ e C R Z J D c = D e D e = J e Z e R
275 265 274 eqtrd φ e C R Z J D c = D e D c = J e Z e R
276 275 fveq2d φ e C R Z J D c = D e 2 nd D c = 2 nd J e Z e R
277 276 adantlrl φ c C R Z J e C R Z J D c = D e 2 nd D c = 2 nd J e Z e R
278 277 adantr φ c C R Z J e C R Z J D c = D e t R 2 nd D c = 2 nd J e Z e R
279 ovex J e Z V
280 vex e V
281 280 resex e R V
282 279 281 op2nd 2 nd J e Z e R = e R
283 282 a1i φ c C R Z J e C R Z J D c = D e t R 2 nd J e Z e R = e R
284 278 283 eqtrd φ c C R Z J e C R Z J D c = D e t R 2 nd D c = e R
285 284 fveq1d φ c C R Z J e C R Z J D c = D e t R 2 nd D c t = e R t
286 fvres t R e R t = e t
287 286 adantl φ c C R Z J e C R Z J D c = D e t R e R t = e t
288 285 287 eqtrd φ c C R Z J e C R Z J D c = D e t R 2 nd D c t = e t
289 251 264 288 3eqtrd φ c C R Z J e C R Z J D c = D e t R c t = e t
290 289 adantlr φ c C R Z J e C R Z J D c = D e t R Z t R c t = e t
291 simpl φ c C R Z J e C R Z J D c = D e t R Z ¬ t R φ c C R Z J e C R Z J D c = D e t R Z
292 elunnel1 t R Z ¬ t R t Z
293 elsni t Z t = Z
294 292 293 syl t R Z ¬ t R t = Z
295 294 adantll φ c C R Z J e C R Z J D c = D e t R Z ¬ t R t = Z
296 simpr φ c C R Z J e C R Z J D c = D e t = Z t = Z
297 296 fveq2d φ c C R Z J e C R Z J D c = D e t = Z c t = c Z
298 2 nn0cnd φ J
299 298 adantr φ c C R Z J J
300 299 125 nncand φ c C R Z J J J c Z = c Z
301 300 eqcomd φ c C R Z J c Z = J J c Z
302 301 adantrr φ c C R Z J e C R Z J c Z = J J c Z
303 302 adantr φ c C R Z J e C R Z J D c = D e c Z = J J c Z
304 255 fveq2d φ c C R Z J 1 st D c = 1 st J c Z c R
305 258 226 op1st 1 st J c Z c R = J c Z
306 305 a1i φ c C R Z J 1 st J c Z c R = J c Z
307 304 306 eqtr2d φ c C R Z J J c Z = 1 st D c
308 307 oveq2d φ c C R Z J J J c Z = J 1 st D c
309 308 adantrr φ c C R Z J e C R Z J J J c Z = J 1 st D c
310 309 adantr φ c C R Z J e C R Z J D c = D e J J c Z = J 1 st D c
311 fveq2 D c = D e 1 st D c = 1 st D e
312 311 adantl φ e C R Z J D c = D e 1 st D c = 1 st D e
313 273 fveq2d φ e C R Z J 1 st D e = 1 st J e Z e R
314 313 adantr φ e C R Z J D c = D e 1 st D e = 1 st J e Z e R
315 279 281 op1st 1 st J e Z e R = J e Z
316 315 a1i φ e C R Z J D c = D e 1 st J e Z e R = J e Z
317 312 314 316 3eqtrd φ e C R Z J D c = D e 1 st D c = J e Z
318 317 oveq2d φ e C R Z J D c = D e J 1 st D c = J J e Z
319 298 adantr φ e C R Z J J
320 zsscn
321 107 320 sstri 0 J
322 321 a1i φ e C R Z J 0 J
323 eleq1w c = e c C R Z J e C R Z J
324 323 anbi2d c = e φ c C R Z J φ e C R Z J
325 feq1 c = e c : R Z 0 J e : R Z 0 J
326 324 325 imbi12d c = e φ c C R Z J c : R Z 0 J φ e C R Z J e : R Z 0 J
327 326 48 chvarvv φ e C R Z J e : R Z 0 J
328 52 adantr φ e C R Z J Z R Z
329 327 328 ffvelrnd φ e C R Z J e Z 0 J
330 322 329 sseldd φ e C R Z J e Z
331 319 330 nncand φ e C R Z J J J e Z = e Z
332 331 adantr φ e C R Z J D c = D e J J e Z = e Z
333 eqidd φ e C R Z J D c = D e e Z = e Z
334 318 332 333 3eqtrd φ e C R Z J D c = D e J 1 st D c = e Z
335 334 adantlrl φ c C R Z J e C R Z J D c = D e J 1 st D c = e Z
336 303 310 335 3eqtrd φ c C R Z J e C R Z J D c = D e c Z = e Z
337 336 adantr φ c C R Z J e C R Z J D c = D e t = Z c Z = e Z
338 fveq2 t = Z e t = e Z
339 338 eqcomd t = Z e Z = e t
340 339 adantl φ c C R Z J e C R Z J D c = D e t = Z e Z = e t
341 297 337 340 3eqtrd φ c C R Z J e C R Z J D c = D e t = Z c t = e t
342 341 adantlr φ c C R Z J e C R Z J D c = D e t R Z t = Z c t = e t
343 291 295 342 syl2anc φ c C R Z J e C R Z J D c = D e t R Z ¬ t R c t = e t
344 290 343 pm2.61dan φ c C R Z J e C R Z J D c = D e t R Z c t = e t
345 344 ex φ c C R Z J e C R Z J D c = D e t R Z c t = e t
346 248 345 ralrimi φ c C R Z J e C R Z J D c = D e t R Z c t = e t
347 69 adantrr φ c C R Z J e C R Z J c Fn R Z
348 347 adantr φ c C R Z J e C R Z J D c = D e c Fn R Z
349 327 ffnd φ e C R Z J e Fn R Z
350 349 adantrl φ c C R Z J e C R Z J e Fn R Z
351 350 adantr φ c C R Z J e C R Z J D c = D e e Fn R Z
352 eqfnfv c Fn R Z e Fn R Z c = e t R Z c t = e t
353 348 351 352 syl2anc φ c C R Z J e C R Z J D c = D e c = e t R Z c t = e t
354 346 353 mpbird φ c C R Z J e C R Z J D c = D e c = e
355 354 ex φ c C R Z J e C R Z J D c = D e c = e
356 355 ralrimivva φ c C R Z J e C R Z J D c = D e c = e
357 243 356 jca φ D : C R Z J k = 0 J k × C R k c C R Z J e C R Z J D c = D e c = e
358 dff13 D : C R Z J 1-1 k = 0 J k × C R k D : C R Z J k = 0 J k × C R k c C R Z J e C R Z J D c = D e c = e
359 357 358 sylibr φ D : C R Z J 1-1 k = 0 J k × C R k
360 eliun p k = 0 J k × C R k k 0 J p k × C R k
361 360 biimpi p k = 0 J k × C R k k 0 J p k × C R k
362 361 adantl φ p k = 0 J k × C R k k 0 J p k × C R k
363 nfv k φ
364 nfcv _ k p
365 nfiu1 _ k k = 0 J k × C R k
366 364 365 nfel k p k = 0 J k × C R k
367 363 366 nfan k φ p k = 0 J k × C R k
368 nfv k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
369 nfv t k 0 J
370 nfcv _ t p
371 nfcv _ t k
372 nfcv _ t R
373 86 372 nffv _ t C R
374 nfcv _ t k
375 373 374 nffv _ t C R k
376 371 375 nfxp _ t k × C R k
377 370 376 nfel t p k × C R k
378 74 369 377 nf3an t φ k 0 J p k × C R k
379 0zd φ k 0 J p k × C R k t R Z 0
380 10 adantr φ t R Z J
381 380 3ad2antl1 φ k 0 J p k × C R k t R Z J
382 iftrue t R if t R 2 nd p t J 1 st p = 2 nd p t
383 382 adantl φ k 0 J p k × C R k t R Z t R if t R 2 nd p t J 1 st p = 2 nd p t
384 simp1 φ k 0 J p k × C R k φ
385 simp2 φ k 0 J p k × C R k k 0 J
386 xp2nd p k × C R k 2 nd p C R k
387 386 3ad2ant3 φ k 0 J p k × C R k 2 nd p C R k
388 188 adantr φ k 0 J C R = n 0 c 0 n R | t R c t = n
389 oveq2 n = k 0 n = 0 k
390 389 oveq1d n = k 0 n R = 0 k R
391 rabeq 0 n R = 0 k R c 0 n R | t R c t = n = c 0 k R | t R c t = n
392 390 391 syl n = k c 0 n R | t R c t = n = c 0 k R | t R c t = n
393 eqeq2 n = k t R c t = n t R c t = k
394 393 rabbidv n = k c 0 k R | t R c t = n = c 0 k R | t R c t = k
395 392 394 eqtrd n = k c 0 n R | t R c t = n = c 0 k R | t R c t = k
396 395 adantl φ k 0 J n = k c 0 n R | t R c t = n = c 0 k R | t R c t = k
397 elfznn0 k 0 J k 0
398 397 adantl φ k 0 J k 0
399 ovex 0 k R V
400 399 rabex c 0 k R | t R c t = k V
401 400 a1i φ k 0 J c 0 k R | t R c t = k V
402 388 396 398 401 fvmptd φ k 0 J C R k = c 0 k R | t R c t = k
403 402 3adant3 φ k 0 J p k × C R k C R k = c 0 k R | t R c t = k
404 387 403 eleqtrd φ k 0 J p k × C R k 2 nd p c 0 k R | t R c t = k
405 elrabi 2 nd p c 0 k R | t R c t = k 2 nd p 0 k R
406 405 3ad2ant3 φ k 0 J 2 nd p c 0 k R | t R c t = k 2 nd p 0 k R
407 384 385 404 406 syl3anc φ k 0 J p k × C R k 2 nd p 0 k R
408 elmapi 2 nd p 0 k R 2 nd p : R 0 k
409 407 408 syl φ k 0 J p k × C R k 2 nd p : R 0 k
410 409 adantr φ k 0 J p k × C R k t R Z 2 nd p : R 0 k
411 410 ffvelrnda φ k 0 J p k × C R k t R Z t R 2 nd p t 0 k
412 411 elfzelzd φ k 0 J p k × C R k t R Z t R 2 nd p t
413 383 412 eqeltrd φ k 0 J p k × C R k t R Z t R if t R 2 nd p t J 1 st p
414 simpl φ k 0 J p k × C R k t R Z ¬ t R φ k 0 J p k × C R k t R Z
415 294 adantll φ k 0 J p k × C R k t R Z ¬ t R t = Z
416 simpr φ t = Z t = Z
417 6 adantr φ t = Z ¬ Z R
418 416 417 eqneltrd φ t = Z ¬ t R
419 418 iffalsed φ t = Z if t R 2 nd p t J 1 st p = J 1 st p
420 419 3ad2antl1 φ k 0 J p k × C R k t = Z if t R 2 nd p t J 1 st p = J 1 st p
421 10 adantr φ t = Z J
422 421 3ad2antl1 φ k 0 J p k × C R k t = Z J
423 xp1st p k × C R k 1 st p k
424 elsni 1 st p k 1 st p = k
425 423 424 syl p k × C R k 1 st p = k
426 425 adantl k 0 J p k × C R k 1 st p = k
427 107 sseli k 0 J k
428 427 adantr k 0 J p k × C R k k
429 426 428 eqeltrd k 0 J p k × C R k 1 st p
430 429 3adant1 φ k 0 J p k × C R k 1 st p
431 430 adantr φ k 0 J p k × C R k t = Z 1 st p
432 422 431 zsubcld φ k 0 J p k × C R k t = Z J 1 st p
433 420 432 eqeltrd φ k 0 J p k × C R k t = Z if t R 2 nd p t J 1 st p
434 433 adantlr φ k 0 J p k × C R k t R Z t = Z if t R 2 nd p t J 1 st p
435 414 415 434 syl2anc φ k 0 J p k × C R k t R Z ¬ t R if t R 2 nd p t J 1 st p
436 413 435 pm2.61dan φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p
437 409 ffvelrnda φ k 0 J p k × C R k t R 2 nd p t 0 k
438 elfzle1 2 nd p t 0 k 0 2 nd p t
439 437 438 syl φ k 0 J p k × C R k t R 0 2 nd p t
440 382 eqcomd t R 2 nd p t = if t R 2 nd p t J 1 st p
441 440 adantl φ k 0 J p k × C R k t R 2 nd p t = if t R 2 nd p t J 1 st p
442 439 441 breqtrd φ k 0 J p k × C R k t R 0 if t R 2 nd p t J 1 st p
443 442 adantlr φ k 0 J p k × C R k t R Z t R 0 if t R 2 nd p t J 1 st p
444 simpll φ k 0 J p k × C R k t R Z ¬ t R φ k 0 J p k × C R k
445 elfzle2 k 0 J k J
446 elfzel2 k 0 J J
447 446 zred k 0 J J
448 109 sseli k 0 J k
449 447 448 subge0d k 0 J 0 J k k J
450 445 449 mpbird k 0 J 0 J k
451 450 adantr k 0 J t = Z 0 J k
452 451 3ad2antl2 φ k 0 J p k × C R k t = Z 0 J k
453 384 418 sylan φ k 0 J p k × C R k t = Z ¬ t R
454 453 iffalsed φ k 0 J p k × C R k t = Z if t R 2 nd p t J 1 st p = J 1 st p
455 426 3adant1 φ k 0 J p k × C R k 1 st p = k
456 455 oveq2d φ k 0 J p k × C R k J 1 st p = J k
457 456 adantr φ k 0 J p k × C R k t = Z J 1 st p = J k
458 454 457 eqtr2d φ k 0 J p k × C R k t = Z J k = if t R 2 nd p t J 1 st p
459 452 458 breqtrd φ k 0 J p k × C R k t = Z 0 if t R 2 nd p t J 1 st p
460 444 415 459 syl2anc φ k 0 J p k × C R k t R Z ¬ t R 0 if t R 2 nd p t J 1 st p
461 443 460 pm2.61dan φ k 0 J p k × C R k t R Z 0 if t R 2 nd p t J 1 st p
462 simpl2 φ k 0 J p k × C R k t R k 0 J
463 fzssz 0 k
464 463 sseli 2 nd p t 0 k 2 nd p t
465 464 zred 2 nd p t 0 k 2 nd p t
466 465 adantr 2 nd p t 0 k k 0 J 2 nd p t
467 448 adantl 2 nd p t 0 k k 0 J k
468 447 adantl 2 nd p t 0 k k 0 J J
469 elfzle2 2 nd p t 0 k 2 nd p t k
470 469 adantr 2 nd p t 0 k k 0 J 2 nd p t k
471 445 adantl 2 nd p t 0 k k 0 J k J
472 466 467 468 470 471 letrd 2 nd p t 0 k k 0 J 2 nd p t J
473 437 462 472 syl2anc φ k 0 J p k × C R k t R 2 nd p t J
474 473 adantlr φ k 0 J p k × C R k t R Z t R 2 nd p t J
475 383 474 eqbrtrd φ k 0 J p k × C R k t R Z t R if t R 2 nd p t J 1 st p J
476 458 eqcomd φ k 0 J p k × C R k t = Z if t R 2 nd p t J 1 st p = J k
477 398 nn0ge0d φ k 0 J 0 k
478 447 adantl φ k 0 J J
479 448 adantl φ k 0 J k
480 478 479 subge02d φ k 0 J 0 k J k J
481 477 480 mpbid φ k 0 J J k J
482 481 adantr φ k 0 J t = Z J k J
483 482 3adantl3 φ k 0 J p k × C R k t = Z J k J
484 476 483 eqbrtrd φ k 0 J p k × C R k t = Z if t R 2 nd p t J 1 st p J
485 444 415 484 syl2anc φ k 0 J p k × C R k t R Z ¬ t R if t R 2 nd p t J 1 st p J
486 475 485 pm2.61dan φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p J
487 379 381 436 461 486 elfzd φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p 0 J
488 eqid t R Z if t R 2 nd p t J 1 st p = t R Z if t R 2 nd p t J 1 st p
489 378 487 488 fmptdf φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p : R Z 0 J
490 ovexd φ k 0 J p k × C R k 0 J V
491 384 21 syl φ k 0 J p k × C R k R Z V
492 490 491 elmapd φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p 0 J R Z t R Z if t R 2 nd p t J 1 st p : R Z 0 J
493 489 492 mpbird φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p 0 J R Z
494 eqidd φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p = r R Z if r R 2 nd p r J 1 st p
495 eleq1w r = t r R t R
496 fveq2 r = t 2 nd p r = 2 nd p t
497 495 496 ifbieq1d r = t if r R 2 nd p r J 1 st p = if t R 2 nd p t J 1 st p
498 497 adantl φ k 0 J p k × C R k t R Z r = t if r R 2 nd p r J 1 st p = if t R 2 nd p t J 1 st p
499 simpr φ k 0 J p k × C R k t R Z t R Z
500 494 498 499 436 fvmptd φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p t = if t R 2 nd p t J 1 st p
501 500 ex φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p t = if t R 2 nd p t J 1 st p
502 378 501 ralrimi φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p t = if t R 2 nd p t J 1 st p
503 502 sumeq2d φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p t = t R Z if t R 2 nd p t J 1 st p
504 nfcv _ t if Z R 2 nd p Z J 1 st p
505 384 105 syl φ k 0 J p k × C R k R Fin
506 384 5 syl φ k 0 J p k × C R k Z T
507 384 6 syl φ k 0 J p k × C R k ¬ Z R
508 382 adantl φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p t
509 437 elfzelzd φ k 0 J p k × C R k t R 2 nd p t
510 509 zcnd φ k 0 J p k × C R k t R 2 nd p t
511 508 510 eqeltrd φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p
512 eleq1 t = Z t R Z R
513 fveq2 t = Z 2 nd p t = 2 nd p Z
514 512 513 ifbieq1d t = Z if t R 2 nd p t J 1 st p = if Z R 2 nd p Z J 1 st p
515 6 adantr φ p k × C R k ¬ Z R
516 515 iffalsed φ p k × C R k if Z R 2 nd p Z J 1 st p = J 1 st p
517 516 3adant2 φ k 0 J p k × C R k if Z R 2 nd p Z J 1 st p = J 1 st p
518 10 3ad2ant1 φ k 0 J p k × C R k J
519 518 430 zsubcld φ k 0 J p k × C R k J 1 st p
520 519 zcnd φ k 0 J p k × C R k J 1 st p
521 517 520 eqeltrd φ k 0 J p k × C R k if Z R 2 nd p Z J 1 st p
522 378 504 505 506 507 511 514 521 fsumsplitsn φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p = t R if t R 2 nd p t J 1 st p + if Z R 2 nd p Z J 1 st p
523 382 a1i φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p t
524 378 523 ralrimi φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p t
525 524 sumeq2d φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = t R 2 nd p t
526 eqidd c = 2 nd p R = R
527 simpl c = 2 nd p t R c = 2 nd p
528 527 fveq1d c = 2 nd p t R c t = 2 nd p t
529 526 528 sumeq12rdv c = 2 nd p t R c t = t R 2 nd p t
530 529 eqeq1d c = 2 nd p t R c t = k t R 2 nd p t = k
531 530 elrab 2 nd p c 0 k R | t R c t = k 2 nd p 0 k R t R 2 nd p t = k
532 404 531 sylib φ k 0 J p k × C R k 2 nd p 0 k R t R 2 nd p t = k
533 532 simprd φ k 0 J p k × C R k t R 2 nd p t = k
534 525 533 eqtrd φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = k
535 507 iffalsed φ k 0 J p k × C R k if Z R 2 nd p Z J 1 st p = J 1 st p
536 535 456 eqtrd φ k 0 J p k × C R k if Z R 2 nd p Z J 1 st p = J k
537 534 536 oveq12d φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p + if Z R 2 nd p Z J 1 st p = k + J - k
538 321 sseli k 0 J k
539 538 3ad2ant2 φ k 0 J p k × C R k k
540 384 298 syl φ k 0 J p k × C R k J
541 539 540 pncan3d φ k 0 J p k × C R k k + J - k = J
542 537 541 eqtrd φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p + if Z R 2 nd p Z J 1 st p = J
543 503 522 542 3eqtrd φ k 0 J p k × C R k t R Z r R Z if r R 2 nd p r J 1 st p t = J
544 493 543 jca φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p 0 J R Z t R Z r R Z if r R 2 nd p r J 1 st p t = J
545 eleq1w t = r t R r R
546 fveq2 t = r 2 nd p t = 2 nd p r
547 545 546 ifbieq1d t = r if t R 2 nd p t J 1 st p = if r R 2 nd p r J 1 st p
548 547 cbvmptv t R Z if t R 2 nd p t J 1 st p = r R Z if r R 2 nd p r J 1 st p
549 548 eqeq2i c = t R Z if t R 2 nd p t J 1 st p c = r R Z if r R 2 nd p r J 1 st p
550 549 biimpi c = t R Z if t R 2 nd p t J 1 st p c = r R Z if r R 2 nd p r J 1 st p
551 fveq1 c = r R Z if r R 2 nd p r J 1 st p c t = r R Z if r R 2 nd p r J 1 st p t
552 551 sumeq2sdv c = r R Z if r R 2 nd p r J 1 st p t R Z c t = t R Z r R Z if r R 2 nd p r J 1 st p t
553 550 552 syl c = t R Z if t R 2 nd p t J 1 st p t R Z c t = t R Z r R Z if r R 2 nd p r J 1 st p t
554 553 eqeq1d c = t R Z if t R 2 nd p t J 1 st p t R Z c t = J t R Z r R Z if r R 2 nd p r J 1 st p t = J
555 554 elrab t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J t R Z if t R 2 nd p t J 1 st p 0 J R Z t R Z r R Z if r R 2 nd p r J 1 st p t = J
556 544 555 sylibr φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
557 556 3exp φ k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
558 557 adantr φ p k = 0 J k × C R k k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
559 367 368 558 rexlimd φ p k = 0 J k × C R k k 0 J p k × C R k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
560 362 559 mpd φ p k = 0 J k × C R k t R Z if t R 2 nd p t J 1 st p c 0 J R Z | t R Z c t = J
561 40 eqcomd φ c 0 J R Z | t R Z c t = J = C R Z J
562 561 adantr φ p k = 0 J k × C R k c 0 J R Z | t R Z c t = J = C R Z J
563 560 562 eleqtrd φ p k = 0 J k × C R k t R Z if t R 2 nd p t J 1 st p C R Z J
564 3 a1i φ p k = 0 J k × C R k D = c C R Z J J c Z c R
565 simpr φ c = t R Z if t R 2 nd p t J 1 st p c = t R Z if t R 2 nd p t J 1 st p
566 548 a1i φ c = t R Z if t R 2 nd p t J 1 st p t R Z if t R 2 nd p t J 1 st p = r R Z if r R 2 nd p r J 1 st p
567 565 566 eqtrd φ c = t R Z if t R 2 nd p t J 1 st p c = r R Z if r R 2 nd p r J 1 st p
568 simpr φ r = Z r = Z
569 6 adantr φ r = Z ¬ Z R
570 568 569 eqneltrd φ r = Z ¬ r R
571 570 iffalsed φ r = Z if r R 2 nd p r J 1 st p = J 1 st p
572 571 adantlr φ c = t R Z if t R 2 nd p t J 1 st p r = Z if r R 2 nd p r J 1 st p = J 1 st p
573 52 adantr φ c = t R Z if t R 2 nd p t J 1 st p Z R Z
574 ovexd φ c = t R Z if t R 2 nd p t J 1 st p J 1 st p V
575 567 572 573 574 fvmptd φ c = t R Z if t R 2 nd p t J 1 st p c Z = J 1 st p
576 575 oveq2d φ c = t R Z if t R 2 nd p t J 1 st p J c Z = J J 1 st p
577 576 adantlr φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p J c Z = J J 1 st p
578 298 ad2antrr φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p J
579 nfv k 1 st p 0 J
580 simpl k 0 J p k × C R k k 0 J
581 simpr k 0 J 1 st p = k 1 st p = k
582 simpl k 0 J 1 st p = k k 0 J
583 581 582 eqeltrd k 0 J 1 st p = k 1 st p 0 J
584 580 426 583 syl2anc k 0 J p k × C R k 1 st p 0 J
585 584 ex k 0 J p k × C R k 1 st p 0 J
586 585 a1i p k = 0 J k × C R k k 0 J p k × C R k 1 st p 0 J
587 366 579 586 rexlimd p k = 0 J k × C R k k 0 J p k × C R k 1 st p 0 J
588 361 587 mpd p k = 0 J k × C R k 1 st p 0 J
589 588 elfzelzd p k = 0 J k × C R k 1 st p
590 589 zcnd p k = 0 J k × C R k 1 st p
591 590 ad2antlr φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p 1 st p
592 578 591 nncand φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p J J 1 st p = 1 st p
593 577 592 eqtrd φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p J c Z = 1 st p
594 reseq1 c = t R Z if t R 2 nd p t J 1 st p c R = t R Z if t R 2 nd p t J 1 st p R
595 594 adantl φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p c R = t R Z if t R 2 nd p t J 1 st p R
596 70 a1i φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p R R Z
597 596 resmptd φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p t R Z if t R 2 nd p t J 1 st p R = t R if t R 2 nd p t J 1 st p
598 nfv k t R if t R 2 nd p t J 1 st p = 2 nd p
599 382 mpteq2ia t R if t R 2 nd p t J 1 st p = t R 2 nd p t
600 599 a1i φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = t R 2 nd p t
601 409 feqmptd φ k 0 J p k × C R k 2 nd p = t R 2 nd p t
602 600 601 eqtr4d φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p
603 602 3exp φ k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p
604 603 adantr φ p k = 0 J k × C R k k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p
605 367 598 604 rexlimd φ p k = 0 J k × C R k k 0 J p k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p
606 362 605 mpd φ p k = 0 J k × C R k t R if t R 2 nd p t J 1 st p = 2 nd p
607 606 adantr φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p t R if t R 2 nd p t J 1 st p = 2 nd p
608 595 597 607 3eqtrd φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p c R = 2 nd p
609 593 608 opeq12d φ p k = 0 J k × C R k c = t R Z if t R 2 nd p t J 1 st p J c Z c R = 1 st p 2 nd p
610 opex 1 st p 2 nd p V
611 610 a1i φ p k = 0 J k × C R k 1 st p 2 nd p V
612 564 609 563 611 fvmptd φ p k = 0 J k × C R k D t R Z if t R 2 nd p t J 1 st p = 1 st p 2 nd p
613 nfv k 1 st p 2 nd p = p
614 1st2nd2 p k × C R k p = 1 st p 2 nd p
615 614 eqcomd p k × C R k 1 st p 2 nd p = p
616 615 a1i k 0 J p k × C R k 1 st p 2 nd p = p
617 616 a1i φ p k = 0 J k × C R k k 0 J p k × C R k 1 st p 2 nd p = p
618 367 613 617 rexlimd φ p k = 0 J k × C R k k 0 J p k × C R k 1 st p 2 nd p = p
619 362 618 mpd φ p k = 0 J k × C R k 1 st p 2 nd p = p
620 612 619 eqtr2d φ p k = 0 J k × C R k p = D t R Z if t R 2 nd p t J 1 st p
621 fveq2 c = t R Z if t R 2 nd p t J 1 st p D c = D t R Z if t R 2 nd p t J 1 st p
622 621 rspceeqv t R Z if t R 2 nd p t J 1 st p C R Z J p = D t R Z if t R 2 nd p t J 1 st p c C R Z J p = D c
623 563 620 622 syl2anc φ p k = 0 J k × C R k c C R Z J p = D c
624 623 ralrimiva φ p k = 0 J k × C R k c C R Z J p = D c
625 243 624 jca φ D : C R Z J k = 0 J k × C R k p k = 0 J k × C R k c C R Z J p = D c
626 dffo3 D : C R Z J onto k = 0 J k × C R k D : C R Z J k = 0 J k × C R k p k = 0 J k × C R k c C R Z J p = D c
627 625 626 sylibr φ D : C R Z J onto k = 0 J k × C R k
628 359 627 jca φ D : C R Z J 1-1 k = 0 J k × C R k D : C R Z J onto k = 0 J k × C R k
629 df-f1o D : C R Z J 1-1 onto k = 0 J k × C R k D : C R Z J 1-1 k = 0 J k × C R k D : C R Z J onto k = 0 J k × C R k
630 628 629 sylibr φ D : C R Z J 1-1 onto k = 0 J k × C R k