Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsquadlem2 Unicode version

 Description: Lemma for lgsquad 21094. Count the members of with even coordinates, and combine with lgsquadlem1 21091 to get the total count of lattice points in (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)
Hypotheses
Ref Expression
lgseisen.1
lgseisen.2
lgseisen.3
Assertion
Ref Expression
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,   ,

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lgseisen.1 . . 3
2 lgseisen.2 . . 3
3 lgseisen.3 . . 3
41, 2, 3lgseisen 21090 . 2
5 lgsquad.4 . . . . . 6
65oveq2i 6051 . . . . 5
76sumeq1i 12447 . . . 4
8 oddprm 13144 . . . . . . . . . . . . 13
91, 8syl 16 . . . . . . . . . . . 12
105, 9syl5eqel 2488 . . . . . . . . . . 11
1110nnred 9971 . . . . . . . . . 10
1211rehalfcld 10170 . . . . . . . . 9
1312flcld 11162 . . . . . . . 8
1413zred 10331 . . . . . . 7
1514ltp1d 9897 . . . . . 6
16 fzdisj 11034 . . . . . 6
1715, 16syl 16 . . . . 5
1810nnrpd 10603 . . . . . . . . . . 11
1918rphalfcld 10616 . . . . . . . . . 10
2019rpge0d 10608 . . . . . . . . 9
21 flge0nn0 11180 . . . . . . . . 9
2212, 20, 21syl2anc 643 . . . . . . . 8
2310nnnn0d 10230 . . . . . . . 8
24 rphalflt 10594 . . . . . . . . . . 11
2518, 24syl 16 . . . . . . . . . 10
2610nnzd 10330 . . . . . . . . . . 11
27 fllt 11170 . . . . . . . . . . 11
2812, 26, 27syl2anc 643 . . . . . . . . . 10
2925, 28mpbid 202 . . . . . . . . 9
3014, 11, 29ltled 9177 . . . . . . . 8
31 elfz2nn0 11038 . . . . . . . 8
3222, 23, 30, 31syl3anbrc 1138 . . . . . . 7
33 nn0uz 10476 . . . . . . . . 9
3423, 33syl6eleq 2494 . . . . . . . 8
35 elfzp12 11081 . . . . . . . 8
3634, 35syl 16 . . . . . . 7
3732, 36mpbid 202 . . . . . 6
38 oveq2 6048 . . . . . . . . . 10
39 fz10 11031 . . . . . . . . . 10
4038, 39syl6eq 2452 . . . . . . . . 9
41 oveq1 6047 . . . . . . . . . . 11
42 0p1e1 10049 . . . . . . . . . . 11
4341, 42syl6eq 2452 . . . . . . . . . 10
4443oveq1d 6055 . . . . . . . . 9
4540, 44uneq12d 3462 . . . . . . . 8
46 un0 3612 . . . . . . . . 9
47 uncom 3451 . . . . . . . . 9
4846, 47eqtr3i 2426 . . . . . . . 8
4945, 48syl6reqr 2455 . . . . . . 7
50 fzsplit 11033 . . . . . . . 8
5142oveq1i 6050 . . . . . . . 8
5250, 51eleq2s 2496 . . . . . . 7
5349, 52jaoi 369 . . . . . 6
5437, 53syl 16 . . . . 5
55 fzfid 11267 . . . . 5
562eldifad 3292 . . . . . . . . . . . 12
57 prmnn 13037 . . . . . . . . . . . 12
5856, 57syl 16 . . . . . . . . . . 11
5958nnred 9971 . . . . . . . . . 10
601eldifad 3292 . . . . . . . . . . 11
61 prmnn 13037 . . . . . . . . . . 11
6260, 61syl 16 . . . . . . . . . 10
6359, 62nndivred 10004 . . . . . . . . 9
6463adantr 452 . . . . . . . 8
65 2nn 10089 . . . . . . . . . 10
66 elfznn 11036 . . . . . . . . . . 11
6766adantl 453 . . . . . . . . . 10
68 nnmulcl 9979 . . . . . . . . . 10
6965, 67, 68sylancr 645 . . . . . . . . 9
7069nnred 9971 . . . . . . . 8
7164, 70remulcld 9072 . . . . . . 7
7258nnrpd 10603 . . . . . . . . . . 11
7362nnrpd 10603 . . . . . . . . . . 11
7472, 73rpdivcld 10621 . . . . . . . . . 10
7574adantr 452 . . . . . . . . 9
7669nnrpd 10603 . . . . . . . . 9
7775, 76rpmulcld 10620 . . . . . . . 8
7877rpge0d 10608 . . . . . . 7
79 flge0nn0 11180 . . . . . . 7
8071, 78, 79syl2anc 643 . . . . . 6
8180nn0cnd 10232 . . . . 5
8217, 54, 55, 81fsumsplit 12488 . . . 4
837, 82syl5eqr 2450 . . 3
8483oveq2d 6056 . 2
85 neg1cn 10023 . . . . 5
8685a1i 11 . . . 4
87 fzfid 11267 . . . . 5
88 ssun2 3471 . . . . . . . 8
8988, 54syl5sseqr 3357 . . . . . . 7
9089sselda 3308 . . . . . 6
9190, 80syldan 457 . . . . 5
9287, 91fsumnn0cl 12485 . . . 4
93 fzfid 11267 . . . . 5
94 ssun1 3470 . . . . . . . 8
9594, 54syl5sseqr 3357 . . . . . . 7
9695sselda 3308 . . . . . 6
9796, 80syldan 457 . . . . 5
9893, 97fsumnn0cl 12485 . . . 4
9986, 92, 98expaddd 11480 . . 3
100 fzfid 11267 . . . . . . . . 9
101 xpfi 7337 . . . . . . . . 9
10255, 100, 101syl2anc 643 . . . . . . . 8
103 lgsquad.6 . . . . . . . . 9
104 opabssxp 4909 . . . . . . . . 9
105103, 104eqsstri 3338 . . . . . . . 8
106 ssfi 7288 . . . . . . . 8
107102, 105, 106sylancl 644 . . . . . . 7
108 ssrab2 3388 . . . . . . 7
109 ssfi 7288 . . . . . . 7
110107, 108, 109sylancl 644 . . . . . 6
111 hashcl 11594 . . . . . 6
112110, 111syl 16 . . . . 5
113 ssrab2 3388 . . . . . . 7
114 ssfi 7288 . . . . . . 7
115107, 113, 114sylancl 644 . . . . . 6
116 hashcl 11594 . . . . . 6
117115, 116syl 16 . . . . 5
11886, 112, 117expaddd 11480 . . . 4
11996, 69syldan 457 . . . . . . . . . . 11
120 fzfid 11267 . . . . . . . . . . 11
121 xpsnen2g 7160 . . . . . . . . . . 11
122119, 120, 121syl2anc 643 . . . . . . . . . 10
123 hasheni 11587 . . . . . . . . . 10
124122, 123syl 16 . . . . . . . . 9
125 ssrab2 3388 . . . . . . . . . . . . 13
126103relopabi 4959 . . . . . . . . . . . . 13
127 relss 4922 . . . . . . . . . . . . 13
128125, 126, 127mp2 9 . . . . . . . . . . . 12
129 relxp 4942 . . . . . . . . . . . 12
130103eleq2i 2468 . . . . . . . . . . . . . . . 16
131 opabid 4421 . . . . . . . . . . . . . . . 16
132130, 131bitri 241 . . . . . . . . . . . . . . 15
133 anass 631 . . . . . . . . . . . . . . . . . 18
134 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . 25
13562ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
136134, 135nnmulcld 10003 . . . . . . . . . . . . . . . . . . . . . . . 24
137136nnred 9971 . . . . . . . . . . . . . . . . . . . . . . 23
13858adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
139138, 119nnmulcld 10003 . . . . . . . . . . . . . . . . . . . . . . . . 25
140139adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
141140nnred 9971 . . . . . . . . . . . . . . . . . . . . . . 23
142137, 141ltlend 9174 . . . . . . . . . . . . . . . . . . . . . 22
143119adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144143nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
145135nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146145rehalfcld 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
14711adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148147adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
149 elfzle2 11017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
150149adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151147rehalfcld 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
152 elfzelz 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
153152adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
154 flge 11169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155151, 153, 154syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156150, 155mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157 elfznn 11036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
158157adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159158nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160 2re 10025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162 2pos 10038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
164 lemuldiv2 9846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
165159, 147, 161, 163, 164syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
166156, 165mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
167166adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
168145ltm1d 9899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
169 peano2rem 9323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
170145, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
171160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
172162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
173 ltdiv1 9830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174170, 145, 171, 172, 173syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
175168, 174mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1765, 175syl5eqbr 4205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
177144, 148, 146, 167, 176lelttrd 9184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
178135nnrpd 10603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
179 rphalflt 10594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
180178, 179syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
181144, 146, 145, 177, 180lttrd 9187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
182144, 145ltnled 9176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183181, 182mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26
18460ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
185 prmz 13038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
186184, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
187 dvdsle 12850 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
188186, 143, 187syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189183, 188mtod 170 . . . . . . . . . . . . . . . . . . . . . . . . 25
190 prmrp 13056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
19160, 56, 190syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1923, 191mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
193192ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26
19456ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
195 prmz 13038 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
196194, 195syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
197143nnzd 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
198 coprmdvds 13057 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
199186, 196, 197, 198syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26
200193, 199mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . . 25
201189, 200mtod 170 . . . . . . . . . . . . . . . . . . . . . . . 24
202 nnz 10259 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
203202adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
204 dvdsmul2 12827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
205203, 186, 204syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
206 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207205, 206syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . . 25
208207necon3bd 2604 . . . . . . . . . . . . . . . . . . . . . . . 24
209201, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23
210209biantrud 494 . . . . . . . . . . . . . . . . . . . . . 22
211142, 210bitr4d 248 . . . . . . . . . . . . . . . . . . . . 21
212 nnre 9963 . . . . . . . . . . . . . . . . . . . . . . 23
213212adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
214135nngt0d 9999 . . . . . . . . . . . . . . . . . . . . . 22
215 lemuldiv 9845 . . . . . . . . . . . . . . . . . . . . . 22
216213, 141, 145, 214, 215syl112anc 1188 . . . . . . . . . . . . . . . . . . . . 21
217138adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
218217nncnd 9972 . . . . . . . . . . . . . . . . . . . . . . 23
219143nncnd 9972 . . . . . . . . . . . . . . . . . . . . . . 23
220135nncnd 9972 . . . . . . . . . . . . . . . . . . . . . . 23
221135nnne0d 10000 . . . . . . . . . . . . . . . . . . . . . . 23
222218, 219, 220, 221div23d 9783 . . . . . . . . . . . . . . . . . . . . . 22
223222breq2d 4184 . . . . . . . . . . . . . . . . . . . . 21
224211, 216, 2233bitrd 271 . . . . . . . . . . . . . . . . . . . 20
225217nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
226217nngt0d 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
227 ltmul2 9817 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
228144, 146, 225, 226, 227syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
229177, 228mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26
230 2cn 10026 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
232 2ne0 10039 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
233232a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
234 divass 9652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
235 div23 9653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
236234, 235eqtr3d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
237218, 220, 231, 233, 236syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . 26
238229, 237breqtrd 4196 . . . . . . . . . . . . . . . . . . . . . . . . 25
239225rehalfcld 10170 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
240239, 145remulcld 9072 . . . . . . . . . . . . . . . . . . . . . . . . . 26
241 lttr 9108 . . . . . . . . . . . . . . . . . . . . . . . . . 26
242137, 141, 240, 241syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25
243238, 242mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . . 24
244 ltmul1 9816 . . . . . . . . . . . . . . . . . . . . . . . . 25
245213, 239, 145, 214, 244syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . 24
246243, 245sylibrd 226 . . . . . . . . . . . . . . . . . . . . . . 23
247 peano2rem 9323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
248225, 247syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
249248recnd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
250218, 249, 231, 233divsubdird 9785 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
251 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
252251oveq2i 6051 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
253250, 252syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . . . . . 26
254 ax-1cn 9004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
255 nncan 9286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
256218, 254, 255sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
257256oveq1d 6055 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
258 halflt1 10145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
259257, 258syl6eqbr 4209 . . . . . . . . . . . . . . . . . . . . . . . . . 26
260253, 259eqbrtrrd 4194 . . . . . . . . . . . . . . . . . . . . . . . . 25
261 oddprm 13144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2622, 261syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
263251, 262syl5eqel 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
264263ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
265264nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . 26
266 1re 9046 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
267266a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
268239, 265, 267ltsubadd2d 9580 . . . . . . . . . . . . . . . . . . . . . . . . 25
269260, 268mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . 24
270 peano2re 9195 . . . . . . . . . . . . . . . . . . . . . . . . . 26
271265, 270syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
272 lttr 9108 . . . . . . . . . . . . . . . . . . . . . . . . 25
273213, 239, 271, 272syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24
274269, 273mpan2d 656 . . . . . . . . . . . . . . . . . . . . . . 23
275246, 274syld 42 . . . . . . . . . . . . . . . . . . . . . 22
276 nnleltp1 10285 . . . . . . . . . . . . . . . . . . . . . . 23
277134, 264, 276syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
278275, 277sylibrd 226 . . . . . . . . . . . . . . . . . . . . 21
279278pm4.71rd 617 . . . . . . . . . . . . . . . . . . . 20
28096, 71syldan 457 . . . . . . . . . . . . . . . . . . . . 21
281 flge 11169 . . . . . . . . . . . . . . . . . . . . 21
282280, 202, 281syl2an 464 . . . . . . . . . . . . . . . . . . . 20
283224, 279, 2823bitr3d 275 . . . . . . . . . . . . . . . . . . 19
284283pm5.32da 623 . . . . . . . . . . . . . . . . . 18
285133, 284syl5bb 249 . . . . . . . . . . . . . . . . 17
286285adantr 452 . . . . . . . . . . . . . . . 16
287 simpr 448 . . . . . . . . . . . . . . . . . . . 20
288 nnuz 10477 . . . . . . . . . . . . . . . . . . . . . . . 24
289119, 288syl6eleq 2494 . . . . . . . . . . . . . . . . . . . . . . 23
29026adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
291 elfz5 11007 . . . . . . . . . . . . . . . . . . . . . . 23
292289, 290, 291syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
293166, 292mpbird 224 . . . . . . . . . . . . . . . . . . . . 21
294293adantr 452 . . . . . . . . . . . . . . . . . . . 20
295287, 294eqeltrd 2478 . . . . . . . . . . . . . . . . . . 19
296295biantrurd 495 . . . . . . . . . . . . . . . . . 18
297263nnzd 10330 . . . . . . . . . . . . . . . . . . . 20
298297ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
299 fznn 11070 . . . . . . . . . . . . . . . . . . 19
300298, 299syl 16 . . . . . . . . . . . . . . . . . 18
301296, 300bitr3d 247 . . . . . . . . . . . . . . . . 17
302 oveq1 6047 . . . . . . . . . . . . . . . . . . 19
303119nncnd 9972 . . . . . . . . . . . . . . . . . . . 20
304138nncnd 9972 . . . . . . . . . . . . . . . . . . . 20
305303, 304mulcomd 9065 . . . . . . . . . . . . . . . . . . 19
306302, 305sylan9eqr 2458 . . . . . . . . . . . . . . . . . 18
307306breq2d 4184 . . . . . . . . . . . . . . . . 17
308301, 307anbi12d 692 . . . . . . . . . . . . . . . 16
309280flcld 11162 . . . . . . . . . . . . . . . . . 18
310 fznn 11070 . . . . . . . . . . . . . . . . . 18
311309, 310syl 16 . . . . . . . . . . . . . . . . 17
312311adantr 452 . . . . . . . . . . . . . . . 16
313286, 308, 3123bitr4d 277 . . . . . . . . . . . . . . 15
314132, 313syl5bb 249 . . . . . . . . . . . . . 14
315314pm5.32da 623 . . . . . . . . . . . . 13
316 vex 2919 . . . . . . . . . . . . . . . . . 18
317 vex 2919 . . . . . . . . . . . . . . . . . 18
318316, 317op1std 6316 . . . . . . . . . . . . . . . . 17
319318eqeq2d 2415 . . . . . . . . . . . . . . . 16
320 eqcom 2406 . . . . . . . . . . . . . . . 16
321319, 320syl6bb 253 . . . . . . . . . . . . . . 15
322321elrab 3052 . . . . . . . . . . . . . 14
323 ancom 438 . . . . . . . . . . . . . 14
324322, 323bitri 241 . . . . . . . . . . . . 13
325 opelxp 4867 . . . . . . . . . . . . . 14
326 elsn 3789 . . . . . . . . . . . . . . 15
327326anbi1i 677 . . . . . . . . . . . . . 14
328325, 327bitri 241 . . . . . . . . . . . . 13
329315, 324, 3283bitr4g 280 . . . . . . . . . . . 12
330128, 129, 329eqrelrdv 4931 . . . . . . . . . . 11
331330eqcomd 2409 . . . . . . . . . 10
332331fveq2d 5691 . . . . . . . . 9
333 hashfz1 11585 . . . . . . . . . 10
33497, 333syl 16 . . . . . . . . 9
335124, 332, 3343eqtr3rd 2445 . . . . . . . 8
336335sumeq2dv 12452 . . . . . . 7
337107adantr 452 . . . . . . . . 9
338 ssfi 7288 . . . . . . . . 9
339337, 125, 338sylancl 644 . . . . . . . 8
340 fveq2 5687 . . . . . . . . . . . . . . . 16
341340eqeq2d 2415 . . . . . . . . . . . . . . 15
342341elrab 3052 . . . . . . . . . . . . . 14
343342simprbi 451 . . . . . . . . . . . . 13
344343ad2antll 710 . . . . . . . . . . . 12
345344oveq1d 6055 . . . . . . . . . . 11
346158nncnd 9972 . . . . . . . . . . . . 13
347346adantrr 698 . . . . . . . . . . . 12
348230a1i 11 . . . . . . . . . . . 12
349232a1i 11 . . . . . . . . . . . 12
350347, 348, 349divcan3d 9751 . . . . . . . . . . 11
351345, 350eqtr3d 2438 . . . . . . . . . 10
352351ralrimivva 2758 . . . . . . . . 9
353 invdisj 4161 . . . . . . . . 9 Disj
354352, 353syl 16 . . . . . . . 8 Disj
35593, 339, 354hashiun 12556 . . . . . . 7
356 iunrab 4098 . . . . . . . . 9
357 zcn 10243 . . . . . . . . . . . . . . 15
358357adantl 453 . . . . . . . . . . . . . 14
359 mulcom 9032 . . . . . . . . . . . . . 14
360230, 358, 359sylancr 645 . . . . . . . . . . . . 13
361360eqeq1d 2412 . . . . . . . . . . . 12
362361rexbidva 2683 . . . . . . . . . . 11
363152anim1i 552 . . . . . . . . . . . . 13
364363reximi2 2772 . . . . . . . . . . . 12
365 simprr 734 . . . . . . . . . . . . . . . . . . 19
366 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23
367105, 366sseldi 3306 . . . . . . . . . . . . . . . . . . . . . 22
368 xp1st 6335 . . . . . . . . . . . . . . . . . . . . . 22
369367, 368syl 16 . . . . . . . . . . . . . . . . . . . . 21
370369adantr 452 . . . . . . . . . . . . . . . . . . . 20
371 elfzle2 11017 . . . . . . . . . . . . . . . . . . . 20
372370, 371syl 16 . . . . . . . . . . . . . . . . . . 19
373365, 372eqbrtrd 4192 . . . . . . . . . . . . . . . . . 18
374 zre 10242 . . . . . . . . . . . . . . . . . . . 20
375374ad2antrl 709 . . . . . . . . . . . . . . . . . . 19
37611ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
377160a1i 11 . . . . . . . . . . . . . . . . . . 19
378162a1i 11 . . . . . . . . . . . . . . . . . . 19
379375, 376, 377, 378, 164syl112anc 1188 . . . . . . . . . . . . . . . . . 18
380373, 379mpbid 202 . . . . . . . . . . . . . . . . 17
38112ad2antrr 707 . . . . . . . . . . . . . . . . . 18
382 simprl 733 . . . . . . . . . . . . . . . . . 18
383381, 382, 154syl2anc 643 . . . . . . . . . . . . . . . . 17
384380, 383mpbid 202 . . . . . . . . . . . . . . . 16
385230mul01i 9212 . . . . . . . . . . . . . . . . . . . . 21
386 elfznn 11036 . . . . . . . . . . . . . . . . . . . . . . . 24
387370, 386syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
388365, 387eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . 22
389388nngt0d 9999 . . . . . . . . . . . . . . . . . . . . 21
390385, 389syl5eqbr 4205 . . . . . . . . . . . . . . . . . . . 20
391 0re 9047 . . . . . . . . . . . . . . . . . . . . . 22
392391a1i 11 . . . . . . . . . . . . . . . . . . . . 21
393 ltmul2 9817 . . . . . . . . . . . . . . . . . . . . 21
394392, 375, 377, 378, 393syl112anc 1188 . . . . . . . . . . . . . . . . . . . 20
395390, 394mpbird 224 . . . . . . . . . . . . . . . . . . 19
396 elnnz 10248 . . . . . . . . . . . . . . . . . . 19
397382, 395, 396sylanbrc 646 . . . . . . . . . . . . . . . . . 18
398397, 288syl6eleq 2494 . . . . . . . . . . . . . . . . 17
39913ad2antrr 707 . . . . . . . . . . . . . . . . 17
400 elfz5 11007 . . . . . . . . . . . . . . . . 17
401398, 399, 400syl2anc 643 . . . . . . . . . . . . . . . 16
402384, 401mpbird 224 . . . . . . . . . . . . . . 15
403402, 365jca 519 . . . . . . . . . . . . . 14
404403ex 424 . . . . . . . . . . . . 13
405404reximdv2 2775 . . . . . . . . . . . 12
406364, 405impbid2 196 . . . . . . . . . . 11
407 2z 10268 . . . . . . . . . . . 12
408 elfzelz 11015 . . . . . . . . . . . . 13
409369, 408syl 16 . . . . . . . . . . . 12
410 divides 12809 . . . . . . . . . . . 12