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