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

 Description: Lemma for lgsquad 23632. Count the members of with even coordinates, and combine with lgsquadlem1 23629 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:   ,,P   ,,   ,M   ,N,   ,Q,   ,S   ,M   ,S

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 23628 . 2
5 lgsquad.4 . . . . . 6
65oveq2i 6307 . . . . 5
76sumeq1i 13520 . . . 4
8 oddprm 14339 . . . . . . . . . . . . 13
91, 8syl 16 . . . . . . . . . . . 12
105, 9syl5eqel 2549 . . . . . . . . . . 11
1110nnred 10576 . . . . . . . . . 10
1211rehalfcld 10810 . . . . . . . . 9
1312flcld 11935 . . . . . . . 8
1413zred 10994 . . . . . . 7
1514ltp1d 10501 . . . . . 6
16 fzdisj 11741 . . . . . 6
1715, 16syl 16 . . . . 5
1810nnrpd 11284 . . . . . . . . . . 11
1918rphalfcld 11297 . . . . . . . . . 10
2019rpge0d 11289 . . . . . . . . 9
21 flge0nn0 11954 . . . . . . . . 9
2212, 20, 21syl2anc 661 . . . . . . . 8
2310nnnn0d 10877 . . . . . . . 8
24 rphalflt 11275 . . . . . . . . . . 11
2518, 24syl 16 . . . . . . . . . 10
2610nnzd 10993 . . . . . . . . . . 11
27 fllt 11943 . . . . . . . . . . 11
2812, 26, 27syl2anc 661 . . . . . . . . . 10
2925, 28mpbid 210 . . . . . . . . 9
3014, 11, 29ltled 9754 . . . . . . . 8
31 elfz2nn0 11798 . . . . . . . 8
3222, 23, 30, 31syl3anbrc 1180 . . . . . . 7
33 nn0uz 11144 . . . . . . . . 9
3423, 33syl6eleq 2555 . . . . . . . 8
35 elfzp12 11786 . . . . . . . 8
3634, 35syl 16 . . . . . . 7
3732, 36mpbid 210 . . . . . 6
38 oveq2 6304 . . . . . . . . . 10
39 fz10 11735 . . . . . . . . . 10
4038, 39syl6eq 2514 . . . . . . . . 9
41 oveq1 6303 . . . . . . . . . . 11
42 0p1e1 10672 . . . . . . . . . . 11
4341, 42syl6eq 2514 . . . . . . . . . 10
4443oveq1d 6311 . . . . . . . . 9
4540, 44uneq12d 3658 . . . . . . . 8
46 un0 3810 . . . . . . . . 9
47 uncom 3647 . . . . . . . . 9
4846, 47eqtr3i 2488 . . . . . . . 8
4945, 48syl6reqr 2517 . . . . . . 7
50 fzsplit 11740 . . . . . . . 8
5142oveq1i 6306 . . . . . . . 8
5250, 51eleq2s 2565 . . . . . . 7
5349, 52jaoi 379 . . . . . 6
5437, 53syl 16 . . . . 5
55 fzfid 12083 . . . . 5
562eldifad 3487 . . . . . . . . . . . 12
57 prmnn 14220 . . . . . . . . . . . 12
5856, 57syl 16 . . . . . . . . . . 11
5958nnred 10576 . . . . . . . . . 10
601eldifad 3487 . . . . . . . . . . 11
61 prmnn 14220 . . . . . . . . . . 11
6260, 61syl 16 . . . . . . . . . 10
6359, 62nndivred 10609 . . . . . . . . 9
6463adantr 465 . . . . . . . 8
65 2nn 10718 . . . . . . . . . 10
66 elfznn 11743 . . . . . . . . . . 11
6766adantl 466 . . . . . . . . . 10
68 nnmulcl 10584 . . . . . . . . . 10
6965, 67, 68sylancr 663 . . . . . . . . 9
7069nnred 10576 . . . . . . . 8
7164, 70remulcld 9645 . . . . . . 7
7258nnrpd 11284 . . . . . . . . . . 11
7362nnrpd 11284 . . . . . . . . . . 11
7472, 73rpdivcld 11302 . . . . . . . . . 10
7574adantr 465 . . . . . . . . 9
7669nnrpd 11284 . . . . . . . . 9
7775, 76rpmulcld 11301 . . . . . . . 8
7877rpge0d 11289 . . . . . . 7
79 flge0nn0 11954 . . . . . . 7
8071, 78, 79syl2anc 661 . . . . . 6
8180nn0cnd 10879 . . . . 5
8217, 54, 55, 81fsumsplit 13562 . . . 4
837, 82syl5eqr 2512 . . 3
8483oveq2d 6312 . 2
85 neg1cn 10664 . . . . 5
8685a1i 11 . . . 4
87 fzfid 12083 . . . . 5
88 ssun2 3667 . . . . . . . 8
8988, 54syl5sseqr 3552 . . . . . . 7
9089sselda 3503 . . . . . 6
9190, 80syldan 470 . . . . 5
9287, 91fsumnn0cl 13558 . . . 4
93 fzfid 12083 . . . . 5
94 ssun1 3666 . . . . . . . 8
9594, 54syl5sseqr 3552 . . . . . . 7
9695sselda 3503 . . . . . 6
9796, 80syldan 470 . . . . 5
9893, 97fsumnn0cl 13558 . . . 4
9986, 92, 98expaddd 12312 . . 3
100 fzfid 12083 . . . . . . . . 9
101 xpfi 7811 . . . . . . . . 9
10255, 100, 101syl2anc 661 . . . . . . . 8
103 lgsquad.6 . . . . . . . . 9
104 opabssxp 5079 . . . . . . . . 9
105103, 104eqsstri 3533 . . . . . . . 8
106 ssfi 7760 . . . . . . . 8
107102, 105, 106sylancl 662 . . . . . . 7
108 ssrab2 3584 . . . . . . 7
109 ssfi 7760 . . . . . . 7
110107, 108, 109sylancl 662 . . . . . 6
111 hashcl 12428 . . . . . 6
112110, 111syl 16 . . . . 5
113 ssrab2 3584 . . . . . . 7
114 ssfi 7760 . . . . . . 7
115107, 113, 114sylancl 662 . . . . . 6
116 hashcl 12428 . . . . . 6
117115, 116syl 16 . . . . 5
11886, 112, 117expaddd 12312 . . . 4
11996, 69syldan 470 . . . . . . . . . . 11
120 fzfid 12083 . . . . . . . . . . 11
121 xpsnen2g 7630 . . . . . . . . . . 11
122119, 120, 121syl2anc 661 . . . . . . . . . 10
123 hasheni 12421 . . . . . . . . . 10
124122, 123syl 16 . . . . . . . . 9
125 ssrab2 3584 . . . . . . . . . . . . 13
126103relopabi 5133 . . . . . . . . . . . . 13
127 relss 5095 . . . . . . . . . . . . 13
128125, 126, 127mp2 9 . . . . . . . . . . . 12
129 relxp 5115 . . . . . . . . . . . 12
130103eleq2i 2535 . . . . . . . . . . . . . . . 16
131 opabid 4759 . . . . . . . . . . . . . . . 16
132130, 131bitri 249 . . . . . . . . . . . . . . 15
133 anass 649 . . . . . . . . . . . . . . . . . 18
134 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25
13562ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
136134, 135nnmulcld 10608 . . . . . . . . . . . . . . . . . . . . . . . 24
137136nnred 10576 . . . . . . . . . . . . . . . . . . . . . . 23
13858adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
139138, 119nnmulcld 10608 . . . . . . . . . . . . . . . . . . . . . . . . 25
140139adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
141140nnred 10576 . . . . . . . . . . . . . . . . . . . . . . 23
142137, 141ltlend 9751 . . . . . . . . . . . . . . . . . . . . . 22
143119adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144143nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
145135nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146145rehalfcld 10810 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
14711adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148147adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
149 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
150149adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151147rehalfcld 10810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
152 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
153152adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
154 flge 11942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155151, 153, 154syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156150, 155mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157 elfznn 11743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
158157adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159158nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
160 2re 10630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162 2pos 10652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
164 lemuldiv2 10450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
165159, 147, 161, 163, 164syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
166156, 165mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
167166adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
168145ltm1d 10503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
169 peano2rem 9909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
170145, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
171160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
172162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
173 ltdiv1 10431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174170, 145, 171, 172, 173syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
175168, 174mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1765, 175syl5eqbr 4485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
177144, 148, 146, 167, 176lelttrd 9761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
178135nnrpd 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
179 rphalflt 11275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
180178, 179syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
181144, 146, 145, 177, 180lttrd 9764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
182144, 145ltnled 9753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183181, 182mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
18460ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
185 prmz 14221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
186184, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
187 dvdsle 14031 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
188186, 143, 187syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189183, 188mtod 177 . . . . . . . . . . . . . . . . . . . . . . . . 25
190 prmrp 14242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
19160, 56, 190syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1923, 191mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
193192ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
19456ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
195 prmz 14221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
196194, 195syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
197143nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
198 coprmdvds 14243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
199186, 196, 197, 198syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . 26
200193, 199mpan2d 674 . . . . . . . . . . . . . . . . . . . . . . . . 25
201189, 200mtod 177 . . . . . . . . . . . . . . . . . . . . . . . 24
202 nnz 10911 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
203202adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
204 dvdsmul2 14006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
205203, 186, 204syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
206 breq2 4456 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207205, 206syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . . . . . . 25
208207necon3bd 2669 . . . . . . . . . . . . . . . . . . . . . . . 24
209201, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23
210209biantrud 507 . . . . . . . . . . . . . . . . . . . . . 22
211142, 210bitr4d 256 . . . . . . . . . . . . . . . . . . . . 21
212 nnre 10568 . . . . . . . . . . . . . . . . . . . . . . 23
213212adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
214135nngt0d 10604 . . . . . . . . . . . . . . . . . . . . . 22
215 lemuldiv 10449 . . . . . . . . . . . . . . . . . . . . . 22
216213, 141, 145, 214, 215syl112anc 1232 . . . . . . . . . . . . . . . . . . . . 21
217138adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
218217nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . 23
219143nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . 23
220135nncnd 10577 . . . . . . . . . . . . . . . . . . . . . . 23
221135nnne0d 10605 . . . . . . . . . . . . . . . . . . . . . . 23
222218, 219, 220, 221div23d 10382 . . . . . . . . . . . . . . . . . . . . . 22
223222breq2d 4464 . . . . . . . . . . . . . . . . . . . . 21
224211, 216, 2233bitrd 279 . . . . . . . . . . . . . . . . . . . 20
225217nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
226217nngt0d 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
227 ltmul2 10418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
228144, 146, 225, 226, 227syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
229177, 228mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
230 2cnd 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
231 2ne0 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
232231a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
233 divass 10250 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
234 div23 10251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
235233, 234eqtr3d 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
236218, 220, 230, 232, 235syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
237229, 236breqtrd 4476 . . . . . . . . . . . . . . . . . . . . . . . . 25
238225rehalfcld 10810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
239238, 145remulcld 9645 . . . . . . . . . . . . . . . . . . . . . . . . . 26
240 lttr 9682 . . . . . . . . . . . . . . . . . . . . . . . . . 26
241137, 141, 239, 240syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . 25
242237, 241mpan2d 674 . . . . . . . . . . . . . . . . . . . . . . . 24
243 ltmul1 10417 . . . . . . . . . . . . . . . . . . . . . . . . 25
244213, 238, 145, 214, 243syl112anc 1232 . . . . . . . . . . . . . . . . . . . . . . . 24
245242, 244sylibrd 234 . . . . . . . . . . . . . . . . . . . . . . 23
246 peano2rem 9909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
247225, 246syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
248247recnd 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
249218, 248, 230, 232divsubdird 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
250 lgsquad.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
251250oveq2i 6307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
252249, 251syl6eqr 2516 . . . . . . . . . . . . . . . . . . . . . . . . . 26
253 ax-1cn 9571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254 nncan 9871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
255218, 253, 254sylancl 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
256255oveq1d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27