Metamath Proof Explorer


Theorem lgsquadlem2

Description: Lemma for lgsquad . Count the members of S with even coordinates, and combine with lgsquadlem1 to get the total count of lattice points in S (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses lgseisen.1 φ P 2
lgseisen.2 φ Q 2
lgseisen.3 φ P Q
lgsquad.4 M = P 1 2
lgsquad.5 N = Q 1 2
lgsquad.6 S = x y | x 1 M y 1 N y P < x Q
Assertion lgsquadlem2 φ Q / L P = 1 S

Proof

Step Hyp Ref Expression
1 lgseisen.1 φ P 2
2 lgseisen.2 φ Q 2
3 lgseisen.3 φ P Q
4 lgsquad.4 M = P 1 2
5 lgsquad.5 N = Q 1 2
6 lgsquad.6 S = x y | x 1 M y 1 N y P < x Q
7 1 2 3 lgseisen φ Q / L P = 1 u = 1 P 1 2 Q P 2 u
8 4 oveq2i 1 M = 1 P 1 2
9 8 sumeq1i u = 1 M Q P 2 u = u = 1 P 1 2 Q P 2 u
10 1 4 gausslemma2dlem0b φ M
11 10 nnred φ M
12 11 rehalfcld φ M 2
13 12 flcld φ M 2
14 13 zred φ M 2
15 14 ltp1d φ M 2 < M 2 + 1
16 fzdisj M 2 < M 2 + 1 1 M 2 M 2 + 1 M =
17 15 16 syl φ 1 M 2 M 2 + 1 M =
18 10 nnrpd φ M +
19 18 rphalfcld φ M 2 +
20 19 rpge0d φ 0 M 2
21 flge0nn0 M 2 0 M 2 M 2 0
22 12 20 21 syl2anc φ M 2 0
23 10 nnnn0d φ M 0
24 rphalflt M + M 2 < M
25 18 24 syl φ M 2 < M
26 10 nnzd φ M
27 fllt M 2 M M 2 < M M 2 < M
28 12 26 27 syl2anc φ M 2 < M M 2 < M
29 25 28 mpbid φ M 2 < M
30 14 11 29 ltled φ M 2 M
31 elfz2nn0 M 2 0 M M 2 0 M 0 M 2 M
32 22 23 30 31 syl3anbrc φ M 2 0 M
33 nn0uz 0 = 0
34 23 33 eleqtrdi φ M 0
35 elfzp12 M 0 M 2 0 M M 2 = 0 M 2 0 + 1 M
36 34 35 syl φ M 2 0 M M 2 = 0 M 2 0 + 1 M
37 32 36 mpbid φ M 2 = 0 M 2 0 + 1 M
38 un0 1 M = 1 M
39 uncom 1 M = 1 M
40 38 39 eqtr3i 1 M = 1 M
41 oveq2 M 2 = 0 1 M 2 = 1 0
42 fz10 1 0 =
43 41 42 eqtrdi M 2 = 0 1 M 2 =
44 oveq1 M 2 = 0 M 2 + 1 = 0 + 1
45 0p1e1 0 + 1 = 1
46 44 45 eqtrdi M 2 = 0 M 2 + 1 = 1
47 46 oveq1d M 2 = 0 M 2 + 1 M = 1 M
48 43 47 uneq12d M 2 = 0 1 M 2 M 2 + 1 M = 1 M
49 40 48 eqtr4id M 2 = 0 1 M = 1 M 2 M 2 + 1 M
50 fzsplit M 2 1 M 1 M = 1 M 2 M 2 + 1 M
51 45 oveq1i 0 + 1 M = 1 M
52 50 51 eleq2s M 2 0 + 1 M 1 M = 1 M 2 M 2 + 1 M
53 49 52 jaoi M 2 = 0 M 2 0 + 1 M 1 M = 1 M 2 M 2 + 1 M
54 37 53 syl φ 1 M = 1 M 2 M 2 + 1 M
55 fzfid φ 1 M Fin
56 2 gausslemma2dlem0a φ Q
57 56 nnred φ Q
58 1 gausslemma2dlem0a φ P
59 57 58 nndivred φ Q P
60 59 adantr φ u 1 M Q P
61 2nn 2
62 elfznn u 1 M u
63 62 adantl φ u 1 M u
64 nnmulcl 2 u 2 u
65 61 63 64 sylancr φ u 1 M 2 u
66 65 nnred φ u 1 M 2 u
67 60 66 remulcld φ u 1 M Q P 2 u
68 56 nnrpd φ Q +
69 58 nnrpd φ P +
70 68 69 rpdivcld φ Q P +
71 70 adantr φ u 1 M Q P +
72 65 nnrpd φ u 1 M 2 u +
73 71 72 rpmulcld φ u 1 M Q P 2 u +
74 73 rpge0d φ u 1 M 0 Q P 2 u
75 flge0nn0 Q P 2 u 0 Q P 2 u Q P 2 u 0
76 67 74 75 syl2anc φ u 1 M Q P 2 u 0
77 76 nn0cnd φ u 1 M Q P 2 u
78 17 54 55 77 fsumsplit φ u = 1 M Q P 2 u = u = 1 M 2 Q P 2 u + u = M 2 + 1 M Q P 2 u
79 9 78 syl5eqr φ u = 1 P 1 2 Q P 2 u = u = 1 M 2 Q P 2 u + u = M 2 + 1 M Q P 2 u
80 79 oveq2d φ 1 u = 1 P 1 2 Q P 2 u = 1 u = 1 M 2 Q P 2 u + u = M 2 + 1 M Q P 2 u
81 neg1cn 1
82 81 a1i φ 1
83 fzfid φ M 2 + 1 M Fin
84 ssun2 M 2 + 1 M 1 M 2 M 2 + 1 M
85 84 54 sseqtrrid φ M 2 + 1 M 1 M
86 85 sselda φ u M 2 + 1 M u 1 M
87 86 76 syldan φ u M 2 + 1 M Q P 2 u 0
88 83 87 fsumnn0cl φ u = M 2 + 1 M Q P 2 u 0
89 fzfid φ 1 M 2 Fin
90 ssun1 1 M 2 1 M 2 M 2 + 1 M
91 90 54 sseqtrrid φ 1 M 2 1 M
92 91 sselda φ u 1 M 2 u 1 M
93 92 76 syldan φ u 1 M 2 Q P 2 u 0
94 89 93 fsumnn0cl φ u = 1 M 2 Q P 2 u 0
95 82 88 94 expaddd φ 1 u = 1 M 2 Q P 2 u + u = M 2 + 1 M Q P 2 u = 1 u = 1 M 2 Q P 2 u 1 u = M 2 + 1 M Q P 2 u
96 fzfid φ 1 N Fin
97 xpfi 1 M Fin 1 N Fin 1 M × 1 N Fin
98 55 96 97 syl2anc φ 1 M × 1 N Fin
99 opabssxp x y | x 1 M y 1 N y P < x Q 1 M × 1 N
100 6 99 eqsstri S 1 M × 1 N
101 ssfi 1 M × 1 N Fin S 1 M × 1 N S Fin
102 98 100 101 sylancl φ S Fin
103 ssrab2 z S | ¬ 2 1 st z S
104 ssfi S Fin z S | ¬ 2 1 st z S z S | ¬ 2 1 st z Fin
105 102 103 104 sylancl φ z S | ¬ 2 1 st z Fin
106 hashcl z S | ¬ 2 1 st z Fin z S | ¬ 2 1 st z 0
107 105 106 syl φ z S | ¬ 2 1 st z 0
108 ssrab2 z S | 2 1 st z S
109 ssfi S Fin z S | 2 1 st z S z S | 2 1 st z Fin
110 102 108 109 sylancl φ z S | 2 1 st z Fin
111 hashcl z S | 2 1 st z Fin z S | 2 1 st z 0
112 110 111 syl φ z S | 2 1 st z 0
113 82 107 112 expaddd φ 1 z S | 2 1 st z + z S | ¬ 2 1 st z = 1 z S | 2 1 st z 1 z S | ¬ 2 1 st z
114 92 65 syldan φ u 1 M 2 2 u
115 fzfid φ u 1 M 2 1 Q P 2 u Fin
116 xpsnen2g 2 u 1 Q P 2 u Fin 2 u × 1 Q P 2 u 1 Q P 2 u
117 114 115 116 syl2anc φ u 1 M 2 2 u × 1 Q P 2 u 1 Q P 2 u
118 hasheni 2 u × 1 Q P 2 u 1 Q P 2 u 2 u × 1 Q P 2 u = 1 Q P 2 u
119 117 118 syl φ u 1 M 2 2 u × 1 Q P 2 u = 1 Q P 2 u
120 ssrab2 z S | 2 u = 1 st z S
121 6 relopabi Rel S
122 relss z S | 2 u = 1 st z S Rel S Rel z S | 2 u = 1 st z
123 120 121 122 mp2 Rel z S | 2 u = 1 st z
124 relxp Rel 2 u × 1 Q P 2 u
125 6 eleq2i x y S x y x y | x 1 M y 1 N y P < x Q
126 opabidw x y x y | x 1 M y 1 N y P < x Q x 1 M y 1 N y P < x Q
127 125 126 bitri x y S x 1 M y 1 N y P < x Q
128 anass y y N y P < Q 2 u y y N y P < Q 2 u
129 114 adantr φ u 1 M 2 y 2 u
130 129 nnred φ u 1 M 2 y 2 u
131 58 ad2antrr φ u 1 M 2 y P
132 131 nnred φ u 1 M 2 y P
133 132 rehalfcld φ u 1 M 2 y P 2
134 11 adantr φ u 1 M 2 M
135 134 adantr φ u 1 M 2 y M
136 elfzle2 u 1 M 2 u M 2
137 136 adantl φ u 1 M 2 u M 2
138 134 rehalfcld φ u 1 M 2 M 2
139 elfzelz u 1 M 2 u
140 139 adantl φ u 1 M 2 u
141 flge M 2 u u M 2 u M 2
142 138 140 141 syl2anc φ u 1 M 2 u M 2 u M 2
143 137 142 mpbird φ u 1 M 2 u M 2
144 elfznn u 1 M 2 u
145 144 adantl φ u 1 M 2 u
146 145 nnred φ u 1 M 2 u
147 2re 2
148 147 a1i φ u 1 M 2 2
149 2pos 0 < 2
150 149 a1i φ u 1 M 2 0 < 2
151 lemuldiv2 u M 2 0 < 2 2 u M u M 2
152 146 134 148 150 151 syl112anc φ u 1 M 2 2 u M u M 2
153 143 152 mpbird φ u 1 M 2 2 u M
154 153 adantr φ u 1 M 2 y 2 u M
155 132 ltm1d φ u 1 M 2 y P 1 < P
156 peano2rem P P 1
157 132 156 syl φ u 1 M 2 y P 1
158 147 a1i φ u 1 M 2 y 2
159 149 a1i φ u 1 M 2 y 0 < 2
160 ltdiv1 P 1 P 2 0 < 2 P 1 < P P 1 2 < P 2
161 157 132 158 159 160 syl112anc φ u 1 M 2 y P 1 < P P 1 2 < P 2
162 155 161 mpbid φ u 1 M 2 y P 1 2 < P 2
163 4 162 eqbrtrid φ u 1 M 2 y M < P 2
164 130 135 133 154 163 lelttrd φ u 1 M 2 y 2 u < P 2
165 131 nnrpd φ u 1 M 2 y P +
166 rphalflt P + P 2 < P
167 165 166 syl φ u 1 M 2 y P 2 < P
168 130 133 132 164 167 lttrd φ u 1 M 2 y 2 u < P
169 130 132 ltnled φ u 1 M 2 y 2 u < P ¬ P 2 u
170 168 169 mpbid φ u 1 M 2 y ¬ P 2 u
171 1 eldifad φ P
172 171 ad2antrr φ u 1 M 2 y P
173 prmz P P
174 172 173 syl φ u 1 M 2 y P
175 dvdsle P 2 u P 2 u P 2 u
176 174 129 175 syl2anc φ u 1 M 2 y P 2 u P 2 u
177 170 176 mtod φ u 1 M 2 y ¬ P 2 u
178 2 eldifad φ Q
179 prmrp P Q P gcd Q = 1 P Q
180 171 178 179 syl2anc φ P gcd Q = 1 P Q
181 3 180 mpbird φ P gcd Q = 1
182 181 ad2antrr φ u 1 M 2 y P gcd Q = 1
183 178 ad2antrr φ u 1 M 2 y Q
184 prmz Q Q
185 183 184 syl φ u 1 M 2 y Q
186 129 nnzd φ u 1 M 2 y 2 u
187 coprmdvds P Q 2 u P Q 2 u P gcd Q = 1 P 2 u
188 174 185 186 187 syl3anc φ u 1 M 2 y P Q 2 u P gcd Q = 1 P 2 u
189 182 188 mpan2d φ u 1 M 2 y P Q 2 u P 2 u
190 177 189 mtod φ u 1 M 2 y ¬ P Q 2 u
191 nnz y y
192 191 adantl φ u 1 M 2 y y
193 dvdsmul2 y P P y P
194 192 174 193 syl2anc φ u 1 M 2 y P y P
195 breq2 Q 2 u = y P P Q 2 u P y P
196 194 195 syl5ibrcom φ u 1 M 2 y Q 2 u = y P P Q 2 u
197 196 necon3bd φ u 1 M 2 y ¬ P Q 2 u Q 2 u y P
198 190 197 mpd φ u 1 M 2 y Q 2 u y P
199 simpr φ u 1 M 2 y y
200 199 131 nnmulcld φ u 1 M 2 y y P
201 200 nnred φ u 1 M 2 y y P
202 56 adantr φ u 1 M 2 Q
203 202 114 nnmulcld φ u 1 M 2 Q 2 u
204 203 adantr φ u 1 M 2 y Q 2 u
205 204 nnred φ u 1 M 2 y Q 2 u
206 201 205 ltlend φ u 1 M 2 y y P < Q 2 u y P Q 2 u Q 2 u y P
207 198 206 mpbiran2d φ u 1 M 2 y y P < Q 2 u y P Q 2 u
208 nnre y y
209 208 adantl φ u 1 M 2 y y
210 131 nngt0d φ u 1 M 2 y 0 < P
211 lemuldiv y Q 2 u P 0 < P y P Q 2 u y Q 2 u P
212 209 205 132 210 211 syl112anc φ u 1 M 2 y y P Q 2 u y Q 2 u P
213 202 adantr φ u 1 M 2 y Q
214 213 nncnd φ u 1 M 2 y Q
215 129 nncnd φ u 1 M 2 y 2 u
216 131 nncnd φ u 1 M 2 y P
217 131 nnne0d φ u 1 M 2 y P 0
218 214 215 216 217 div23d φ u 1 M 2 y Q 2 u P = Q P 2 u
219 218 breq2d φ u 1 M 2 y y Q 2 u P y Q P 2 u
220 207 212 219 3bitrd φ u 1 M 2 y y P < Q 2 u y Q P 2 u
221 213 nnred φ u 1 M 2 y Q
222 213 nngt0d φ u 1 M 2 y 0 < Q
223 ltmul2 2 u P 2 Q 0 < Q 2 u < P 2 Q 2 u < Q P 2
224 130 133 221 222 223 syl112anc φ u 1 M 2 y 2 u < P 2 Q 2 u < Q P 2
225 164 224 mpbid φ u 1 M 2 y Q 2 u < Q P 2
226 2cnd φ u 1 M 2 y 2
227 2ne0 2 0
228 227 a1i φ u 1 M 2 y 2 0
229 divass Q P 2 2 0 Q P 2 = Q P 2
230 div23 Q P 2 2 0 Q P 2 = Q 2 P
231 229 230 eqtr3d Q P 2 2 0 Q P 2 = Q 2 P
232 214 216 226 228 231 syl112anc φ u 1 M 2 y Q P 2 = Q 2 P
233 225 232 breqtrd φ u 1 M 2 y Q 2 u < Q 2 P
234 221 rehalfcld φ u 1 M 2 y Q 2
235 234 132 remulcld φ u 1 M 2 y Q 2 P
236 lttr y P Q 2 u Q 2 P y P < Q 2 u Q 2 u < Q 2 P y P < Q 2 P
237 201 205 235 236 syl3anc φ u 1 M 2 y y P < Q 2 u Q 2 u < Q 2 P y P < Q 2 P
238 233 237 mpan2d φ u 1 M 2 y y P < Q 2 u y P < Q 2 P
239 ltmul1 y Q 2 P 0 < P y < Q 2 y P < Q 2 P
240 209 234 132 210 239 syl112anc φ u 1 M 2 y y < Q 2 y P < Q 2 P
241 238 240 sylibrd φ u 1 M 2 y y P < Q 2 u y < Q 2
242 peano2rem Q Q 1
243 221 242 syl φ u 1 M 2 y Q 1
244 243 recnd φ u 1 M 2 y Q 1
245 214 244 226 228 divsubdird φ u 1 M 2 y Q Q 1 2 = Q 2 Q 1 2
246 5 oveq2i Q 2 N = Q 2 Q 1 2
247 245 246 eqtr4di φ u 1 M 2 y Q Q 1 2 = Q 2 N
248 ax-1cn 1
249 nncan Q 1 Q Q 1 = 1
250 214 248 249 sylancl φ u 1 M 2 y Q Q 1 = 1
251 250 oveq1d φ u 1 M 2 y Q Q 1 2 = 1 2
252 halflt1 1 2 < 1
253 251 252 eqbrtrdi φ u 1 M 2 y Q Q 1 2 < 1
254 247 253 eqbrtrrd φ u 1 M 2 y Q 2 N < 1
255 2 5 gausslemma2dlem0b φ N
256 255 ad2antrr φ u 1 M 2 y N
257 256 nnred φ u 1 M 2 y N
258 1red φ u 1 M 2 y 1
259 234 257 258 ltsubadd2d φ u 1 M 2 y Q 2 N < 1 Q 2 < N + 1
260 254 259 mpbid φ u 1 M 2 y Q 2 < N + 1
261 peano2re N N + 1
262 257 261 syl φ u 1 M 2 y N + 1
263 lttr y Q 2 N + 1 y < Q 2 Q 2 < N + 1 y < N + 1
264 209 234 262 263 syl3anc φ u 1 M 2 y y < Q 2 Q 2 < N + 1 y < N + 1
265 260 264 mpan2d φ u 1 M 2 y y < Q 2 y < N + 1
266 241 265 syld φ u 1 M 2 y y P < Q 2 u y < N + 1
267 nnleltp1 y N y N y < N + 1
268 199 256 267 syl2anc φ u 1 M 2 y y N y < N + 1
269 266 268 sylibrd φ u 1 M 2 y y P < Q 2 u y N
270 269 pm4.71rd φ u 1 M 2 y y P < Q 2 u y N y P < Q 2 u
271 92 67 syldan φ u 1 M 2 Q P 2 u
272 flge Q P 2 u y y Q P 2 u y Q P 2 u
273 271 191 272 syl2an φ u 1 M 2 y y Q P 2 u y Q P 2 u
274 220 270 273 3bitr3d φ u 1 M 2 y y N y P < Q 2 u y Q P 2 u
275 274 pm5.32da φ u 1 M 2 y y N y P < Q 2 u y y Q P 2 u
276 128 275 syl5bb φ u 1 M 2 y y N y P < Q 2 u y y Q P 2 u
277 276 adantr φ u 1 M 2 x = 2 u y y N y P < Q 2 u y y Q P 2 u
278 simpr φ u 1 M 2 x = 2 u x = 2 u
279 nnuz = 1
280 114 279 eleqtrdi φ u 1 M 2 2 u 1
281 26 adantr φ u 1 M 2 M
282 elfz5 2 u 1 M 2 u 1 M 2 u M
283 280 281 282 syl2anc φ u 1 M 2 2 u 1 M 2 u M
284 153 283 mpbird φ u 1 M 2 2 u 1 M
285 284 adantr φ u 1 M 2 x = 2 u 2 u 1 M
286 278 285 eqeltrd φ u 1 M 2 x = 2 u x 1 M
287 286 biantrurd φ u 1 M 2 x = 2 u y 1 N x 1 M y 1 N
288 255 nnzd φ N
289 288 ad2antrr φ u 1 M 2 x = 2 u N
290 fznn N y 1 N y y N
291 289 290 syl φ u 1 M 2 x = 2 u y 1 N y y N
292 287 291 bitr3d φ u 1 M 2 x = 2 u x 1 M y 1 N y y N
293 oveq1 x = 2 u x Q = 2 u Q
294 114 nncnd φ u 1 M 2 2 u
295 202 nncnd φ u 1 M 2 Q
296 294 295 mulcomd φ u 1 M 2 2 u Q = Q 2 u
297 293 296 sylan9eqr φ u 1 M 2 x = 2 u x Q = Q 2 u
298 297 breq2d φ u 1 M 2 x = 2 u y P < x Q y P < Q 2 u
299 292 298 anbi12d φ u 1 M 2 x = 2 u x 1 M y 1 N y P < x Q y y N y P < Q 2 u
300 271 flcld φ u 1 M 2 Q P 2 u
301 fznn Q P 2 u y 1 Q P 2 u y y Q P 2 u
302 300 301 syl φ u 1 M 2 y 1 Q P 2 u y y Q P 2 u
303 302 adantr φ u 1 M 2 x = 2 u y 1 Q P 2 u y y Q P 2 u
304 277 299 303 3bitr4d φ u 1 M 2 x = 2 u x 1 M y 1 N y P < x Q y 1 Q P 2 u
305 127 304 syl5bb φ u 1 M 2 x = 2 u x y S y 1 Q P 2 u
306 305 pm5.32da φ u 1 M 2 x = 2 u x y S x = 2 u y 1 Q P 2 u
307 vex x V
308 vex y V
309 307 308 op1std z = x y 1 st z = x
310 309 eqeq2d z = x y 2 u = 1 st z 2 u = x
311 eqcom 2 u = x x = 2 u
312 310 311 syl6bb z = x y 2 u = 1 st z x = 2 u
313 312 elrab x y z S | 2 u = 1 st z x y S x = 2 u
314 313 biancomi x y z S | 2 u = 1 st z x = 2 u x y S
315 opelxp x y 2 u × 1 Q P 2 u x 2 u y 1 Q P 2 u
316 velsn x 2 u x = 2 u
317 316 anbi1i x 2 u y 1 Q P 2 u x = 2 u y 1 Q P 2 u
318 315 317 bitri x y 2 u × 1 Q P 2 u x = 2 u y 1 Q P 2 u
319 306 314 318 3bitr4g φ u 1 M 2 x y z S | 2 u = 1 st z x y 2 u × 1 Q P 2 u
320 123 124 319 eqrelrdv φ u 1 M 2 z S | 2 u = 1 st z = 2 u × 1 Q P 2 u
321 320 eqcomd φ u 1 M 2 2 u × 1 Q P 2 u = z S | 2 u = 1 st z
322 321 fveq2d φ u 1 M 2 2 u × 1 Q P 2 u = z S | 2 u = 1 st z
323 hashfz1 Q P 2 u 0 1 Q P 2 u = Q P 2 u
324 93 323 syl φ u 1 M 2 1 Q P 2 u = Q P 2 u
325 119 322 324 3eqtr3rd φ u 1 M 2 Q P 2 u = z S | 2 u = 1 st z
326 325 sumeq2dv φ u = 1 M 2 Q P 2 u = u = 1 M 2 z S | 2 u = 1 st z
327 102 adantr φ u 1 M 2 S Fin
328 ssfi S Fin z S | 2 u = 1 st z S z S | 2 u = 1 st z Fin
329 327 120 328 sylancl φ u 1 M 2 z S | 2 u = 1 st z Fin
330 fveq2 z = v 1 st z = 1 st v
331 330 eqeq2d z = v 2 u = 1 st z 2 u = 1 st v
332 331 elrab v z S | 2 u = 1 st z v S 2 u = 1 st v
333 332 simprbi v z S | 2 u = 1 st z 2 u = 1 st v
334 333 ad2antll φ u 1 M 2 v z S | 2 u = 1 st z 2 u = 1 st v
335 334 oveq1d φ u 1 M 2 v z S | 2 u = 1 st z 2 u 2 = 1 st v 2
336 145 nncnd φ u 1 M 2 u
337 336 adantrr φ u 1 M 2 v z S | 2 u = 1 st z u
338 2cnd φ u 1 M 2 v z S | 2 u = 1 st z 2
339 227 a1i φ u 1 M 2 v z S | 2 u = 1 st z 2 0
340 337 338 339 divcan3d φ u 1 M 2 v z S | 2 u = 1 st z 2 u 2 = u
341 335 340 eqtr3d φ u 1 M 2 v z S | 2 u = 1 st z 1 st v 2 = u
342 341 ralrimivva φ u 1 M 2 v z S | 2 u = 1 st z 1 st v 2 = u
343 invdisj u 1 M 2 v z S | 2 u = 1 st z 1 st v 2 = u Disj u = 1 M 2 z S | 2 u = 1 st z
344 342 343 syl φ Disj u = 1 M 2 z S | 2 u = 1 st z
345 89 329 344 hashiun φ u = 1 M 2 z S | 2 u = 1 st z = u = 1 M 2 z S | 2 u = 1 st z
346 iunrab u = 1 M 2 z S | 2 u = 1 st z = z S | u 1 M 2 2 u = 1 st z
347 2cn 2
348 zcn u u
349 348 adantl φ z S u u
350 mulcom 2 u 2 u = u 2
351 347 349 350 sylancr φ z S u 2 u = u 2
352 351 eqeq1d φ z S u 2 u = 1 st z u 2 = 1 st z
353 352 rexbidva φ z S u 2 u = 1 st z u u 2 = 1 st z
354 139 anim1i u 1 M 2 2 u = 1 st z u 2 u = 1 st z
355 354 reximi2 u 1 M 2 2 u = 1 st z u 2 u = 1 st z
356 simprr φ z S u 2 u = 1 st z 2 u = 1 st z
357 simpr φ z S z S
358 100 357 sseldi φ z S z 1 M × 1 N
359 xp1st z 1 M × 1 N 1 st z 1 M
360 358 359 syl φ z S 1 st z 1 M
361 360 adantr φ z S u 2 u = 1 st z 1 st z 1 M
362 elfzle2 1 st z 1 M 1 st z M
363 361 362 syl φ z S u 2 u = 1 st z 1 st z M
364 356 363 eqbrtrd φ z S u 2 u = 1 st z 2 u M
365 zre u u
366 365 ad2antrl φ z S u 2 u = 1 st z u
367 11 ad2antrr φ z S u 2 u = 1 st z M
368 147 a1i φ z S u 2 u = 1 st z 2
369 149 a1i φ z S u 2 u = 1 st z 0 < 2
370 366 367 368 369 151 syl112anc φ z S u 2 u = 1 st z 2 u M u M 2
371 364 370 mpbid φ z S u 2 u = 1 st z u M 2
372 12 ad2antrr φ z S u 2 u = 1 st z M 2
373 simprl φ z S u 2 u = 1 st z u
374 372 373 141 syl2anc φ z S u 2 u = 1 st z u M 2 u M 2
375 371 374 mpbid φ z S u 2 u = 1 st z u M 2
376 2t0e0 2 0 = 0
377 elfznn 1 st z 1 M 1 st z
378 361 377 syl φ z S u 2 u = 1 st z 1 st z
379 356 378 eqeltrd φ z S u 2 u = 1 st z 2 u
380 379 nngt0d φ z S u 2 u = 1 st z 0 < 2 u
381 376 380 eqbrtrid φ z S u 2 u = 1 st z 2 0 < 2 u
382 0red φ z S u 2 u = 1 st z 0
383 ltmul2 0 u 2 0 < 2 0 < u 2 0 < 2 u
384 382 366 368 369 383 syl112anc φ z S u 2 u = 1 st z 0 < u 2 0 < 2 u
385 381 384 mpbird φ z S u 2 u = 1 st z 0 < u
386 elnnz u u 0 < u
387 373 385 386 sylanbrc φ z S u 2 u = 1 st z u
388 387 279 eleqtrdi φ z S u 2 u = 1 st z u 1
389 13 ad2antrr φ z S u 2 u = 1 st z M 2
390 elfz5 u 1 M 2 u 1 M 2 u M 2
391 388 389 390 syl2anc φ z S u 2 u = 1 st z u 1 M 2 u M 2
392 375 391 mpbird φ z S u 2 u = 1 st z u 1 M 2
393 392 356 jca φ z S u 2 u = 1 st z u 1 M 2 2 u = 1 st z
394 393 ex φ z S u 2 u = 1 st z u 1 M 2 2 u = 1 st z
395 394 reximdv2 φ z S u 2 u = 1 st z u 1 M 2 2 u = 1 st z
396 355 395 impbid2 φ z S u 1 M 2 2 u = 1 st z u 2 u = 1 st z
397 2z 2
398 elfzelz 1 st z 1 M 1 st z
399 360 398 syl φ z S 1 st z
400 divides 2 1 st z 2 1 st z u u 2 = 1 st z
401 397 399 400 sylancr φ z S 2 1 st z u u 2 = 1 st z
402 353 396 401 3bitr4d φ z S u 1 M 2 2 u = 1 st z 2 1 st z
403 402 rabbidva φ z S | u 1 M 2 2 u = 1 st z = z S | 2 1 st z
404 346 403 syl5eq φ u = 1 M 2 z S | 2 u = 1 st z = z S | 2 1 st z
405 404 fveq2d φ u = 1 M 2 z S | 2 u = 1 st z = z S | 2 1 st z
406 326 345 405 3eqtr2d φ u = 1 M 2 Q P 2 u = z S | 2 1 st z
407 406 oveq2d φ 1 u = 1 M 2 Q P 2 u = 1 z S | 2 1 st z
408 1 2 3 4 5 6 lgsquadlem1 φ 1 u = M 2 + 1 M Q P 2 u = 1 z S | ¬ 2 1 st z
409 407 408 oveq12d φ 1 u = 1 M 2 Q P 2 u 1 u = M 2 + 1 M Q P 2 u = 1 z S | 2 1 st z 1 z S | ¬ 2 1 st z
410 113 409 eqtr4d φ 1 z S | 2 1 st z + z S | ¬ 2 1 st z = 1 u = 1 M 2 Q P 2 u 1 u = M 2 + 1 M Q P 2 u
411 unrab z S | 2 1 st z z S | ¬ 2 1 st z = z S | 2 1 st z ¬ 2 1 st z
412 exmid 2 1 st z ¬ 2 1 st z
413 412 rgenw z S 2 1 st z ¬ 2 1 st z
414 rabid2 S = z S | 2 1 st z ¬ 2 1 st z z S 2 1 st z ¬ 2 1 st z
415 413 414 mpbir S = z S | 2 1 st z ¬ 2 1 st z
416 411 415 eqtr4i z S | 2 1 st z z S | ¬ 2 1 st z = S
417 416 fveq2i z S | 2 1 st z z S | ¬ 2 1 st z = S
418 inrab z S | 2 1 st z z S | ¬ 2 1 st z = z S | 2 1 st z ¬ 2 1 st z
419 pm3.24 ¬ 2 1 st z ¬ 2 1 st z
420 419 a1i φ ¬ 2 1 st z ¬ 2 1 st z
421 420 ralrimivw φ z S ¬ 2 1 st z ¬ 2 1 st z
422 rabeq0 z S | 2 1 st z ¬ 2 1 st z = z S ¬ 2 1 st z ¬ 2 1 st z
423 421 422 sylibr φ z S | 2 1 st z ¬ 2 1 st z =
424 418 423 syl5eq φ z S | 2 1 st z z S | ¬ 2 1 st z =
425 hashun z S | 2 1 st z Fin z S | ¬ 2 1 st z Fin z S | 2 1 st z z S | ¬ 2 1 st z = z S | 2 1 st z z S | ¬ 2 1 st z = z S | 2 1 st z + z S | ¬ 2 1 st z
426 110 105 424 425 syl3anc φ z S | 2 1 st z z S | ¬ 2 1 st z = z S | 2 1 st z + z S | ¬ 2 1 st z
427 417 426 syl5reqr φ z S | 2 1 st z + z S | ¬ 2 1 st z = S
428 427 oveq2d φ 1 z S | 2 1 st z + z S | ¬ 2 1 st z = 1 S
429 95 410 428 3eqtr2d φ 1 u = 1 M 2 Q P 2 u + u = M 2 + 1 M Q P 2 u = 1 S
430 7 80 429 3eqtrd φ Q / L P = 1 S