Metamath Proof Explorer


Theorem ostth3

Description: - Lemma for ostth : p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses qrng.q Q = fld 𝑠
qabsabv.a A = AbsVal Q
padic.j J = q x if x = 0 0 q q pCnt x
ostth.k K = x if x = 0 0 1
ostth.1 φ F A
ostth3.2 φ n ¬ 1 < F n
ostth3.3 φ P
ostth3.4 φ F P < 1
ostth3.5 R = log F P log P
ostth3.6 S = if F P F p F p F P
Assertion ostth3 φ a + F = y J P y a

Proof

Step Hyp Ref Expression
1 qrng.q Q = fld 𝑠
2 qabsabv.a A = AbsVal Q
3 padic.j J = q x if x = 0 0 q q pCnt x
4 ostth.k K = x if x = 0 0 1
5 ostth.1 φ F A
6 ostth3.2 φ n ¬ 1 < F n
7 ostth3.3 φ P
8 ostth3.4 φ F P < 1
9 ostth3.5 R = log F P log P
10 ostth3.6 S = if F P F p F p F P
11 prmuz2 P P 2
12 7 11 syl φ P 2
13 eluz2b2 P 2 P 1 < P
14 12 13 sylib φ P 1 < P
15 14 simpld φ P
16 nnq P P
17 15 16 syl φ P
18 1 qrngbas = Base Q
19 2 18 abvcl F A P F P
20 5 17 19 syl2anc φ F P
21 15 nnne0d φ P 0
22 1 qrng0 0 = 0 Q
23 2 18 22 abvgt0 F A P P 0 0 < F P
24 5 17 21 23 syl3anc φ 0 < F P
25 20 24 elrpd φ F P +
26 25 relogcld φ log F P
27 15 nnred φ P
28 14 simprd φ 1 < P
29 27 28 rplogcld φ log P +
30 26 29 rerpdivcld φ log F P log P
31 30 renegcld φ log F P log P
32 9 31 eqeltrid φ R
33 1rp 1 +
34 logltb F P + 1 + F P < 1 log F P < log 1
35 25 33 34 sylancl φ F P < 1 log F P < log 1
36 8 35 mpbid φ log F P < log 1
37 log1 log 1 = 0
38 36 37 breqtrdi φ log F P < 0
39 29 rpcnd φ log P
40 39 mul01d φ log P 0 = 0
41 38 40 breqtrrd φ log F P < log P 0
42 0red φ 0
43 26 42 29 ltdivmuld φ log F P log P < 0 log F P < log P 0
44 41 43 mpbird φ log F P log P < 0
45 30 lt0neg1d φ log F P log P < 0 0 < log F P log P
46 44 45 mpbid φ 0 < log F P log P
47 46 9 breqtrrdi φ 0 < R
48 32 47 elrpd φ R +
49 1 2 3 padicabvcxp P R + y J P y R A
50 7 48 49 syl2anc φ y J P y R A
51 fveq2 y = P J P y = J P P
52 51 oveq1d y = P J P y R = J P P R
53 eqid y J P y R = y J P y R
54 ovex J P P R V
55 52 53 54 fvmpt P y J P y R P = J P P R
56 17 55 syl φ y J P y R P = J P P R
57 3 padicval P P J P P = if P = 0 0 P P pCnt P
58 7 17 57 syl2anc φ J P P = if P = 0 0 P P pCnt P
59 21 neneqd φ ¬ P = 0
60 59 iffalsed φ if P = 0 0 P P pCnt P = P P pCnt P
61 15 nncnd φ P
62 61 exp1d φ P 1 = P
63 62 oveq2d φ P pCnt P 1 = P pCnt P
64 1z 1
65 pcid P 1 P pCnt P 1 = 1
66 7 64 65 sylancl φ P pCnt P 1 = 1
67 63 66 eqtr3d φ P pCnt P = 1
68 67 negeqd φ P pCnt P = 1
69 68 oveq2d φ P P pCnt P = P 1
70 neg1z 1
71 70 a1i φ 1
72 61 21 71 cxpexpzd φ P 1 = P 1
73 69 72 eqtr4d φ P P pCnt P = P 1
74 58 60 73 3eqtrd φ J P P = P 1
75 74 oveq1d φ J P P R = P 1 R
76 32 recnd φ R
77 76 mulm1d φ -1 R = R
78 9 negeqi R = log F P log P
79 30 recnd φ log F P log P
80 79 negnegd φ log F P log P = log F P log P
81 78 80 eqtrid φ R = log F P log P
82 77 81 eqtrd φ -1 R = log F P log P
83 82 oveq2d φ P -1 R = P log F P log P
84 15 nnrpd φ P +
85 neg1rr 1
86 85 a1i φ 1
87 84 86 76 cxpmuld φ P -1 R = P 1 R
88 61 21 79 cxpefd φ P log F P log P = e log F P log P log P
89 26 recnd φ log F P
90 29 rpne0d φ log P 0
91 89 39 90 divcan1d φ log F P log P log P = log F P
92 91 fveq2d φ e log F P log P log P = e log F P
93 25 reeflogd φ e log F P = F P
94 88 92 93 3eqtrd φ P log F P log P = F P
95 83 87 94 3eqtr3d φ P 1 R = F P
96 56 75 95 3eqtrrd φ F P = y J P y R P
97 fveq2 P = p F P = F p
98 fveq2 P = p y J P y R P = y J P y R p
99 97 98 eqeq12d P = p F P = y J P y R P F p = y J P y R p
100 96 99 syl5ibcom φ P = p F p = y J P y R p
101 100 adantr φ p P = p F p = y J P y R p
102 prmnn p p
103 102 ad2antlr φ p P p p
104 nnq p p
105 103 104 syl φ p P p p
106 fveq2 y = p J P y = J P p
107 106 oveq1d y = p J P y R = J P p R
108 ovex J P p R V
109 107 53 108 fvmpt p y J P y R p = J P p R
110 105 109 syl φ p P p y J P y R p = J P p R
111 76 ad2antrr φ p P p R
112 111 1cxpd φ p P p 1 R = 1
113 7 ad2antrr φ p P p P
114 3 padicval P p J P p = if p = 0 0 P P pCnt p
115 113 105 114 syl2anc φ p P p J P p = if p = 0 0 P P pCnt p
116 103 nnne0d φ p P p p 0
117 116 neneqd φ p P p ¬ p = 0
118 117 iffalsed φ p P p if p = 0 0 P P pCnt p = P P pCnt p
119 pceq0 P p P pCnt p = 0 ¬ P p
120 7 102 119 syl2an φ p P pCnt p = 0 ¬ P p
121 dvdsprm P 2 p P p P = p
122 12 121 sylan φ p P p P = p
123 122 necon3bbid φ p ¬ P p P p
124 120 123 bitrd φ p P pCnt p = 0 P p
125 124 biimpar φ p P p P pCnt p = 0
126 125 negeqd φ p P p P pCnt p = 0
127 neg0 0 = 0
128 126 127 eqtrdi φ p P p P pCnt p = 0
129 128 oveq2d φ p P p P P pCnt p = P 0
130 61 ad2antrr φ p P p P
131 130 exp0d φ p P p P 0 = 1
132 129 131 eqtrd φ p P p P P pCnt p = 1
133 115 118 132 3eqtrd φ p P p J P p = 1
134 133 oveq1d φ p P p J P p R = 1 R
135 2re 2
136 135 a1i φ p P p F p < 1 2
137 5 ad2antrr φ p P p F A
138 2 18 abvcl F A p F p
139 137 105 138 syl2anc φ p P p F p
140 2 18 22 abvgt0 F A p p 0 0 < F p
141 137 105 116 140 syl3anc φ p P p 0 < F p
142 139 141 elrpd φ p P p F p +
143 142 adantrr φ p P p F p < 1 F p +
144 25 ad2antrr φ p P p F p < 1 F P +
145 143 144 ifcld φ p P p F p < 1 if F P F p F p F P +
146 10 145 eqeltrid φ p P p F p < 1 S +
147 146 rprecred φ p P p F p < 1 1 S
148 simprr φ p P p F p < 1 F p < 1
149 8 ad2antrr φ p P p F p < 1 F P < 1
150 breq1 F p = if F P F p F p F P F p < 1 if F P F p F p F P < 1
151 breq1 F P = if F P F p F p F P F P < 1 if F P F p F p F P < 1
152 150 151 ifboth F p < 1 F P < 1 if F P F p F p F P < 1
153 148 149 152 syl2anc φ p P p F p < 1 if F P F p F p F P < 1
154 10 153 eqbrtrid φ p P p F p < 1 S < 1
155 146 reclt1d φ p P p F p < 1 S < 1 1 < 1 S
156 154 155 mpbid φ p P p F p < 1 1 < 1 S
157 expnbnd 2 1 S 1 < 1 S k 2 < 1 S k
158 136 147 156 157 syl3anc φ p P p F p < 1 k 2 < 1 S k
159 146 rpcnd φ p P p F p < 1 S
160 159 adantr φ p P p F p < 1 k S
161 146 rpne0d φ p P p F p < 1 S 0
162 161 adantr φ p P p F p < 1 k S 0
163 nnz k k
164 163 adantl φ p P p F p < 1 k k
165 160 162 164 exprecd φ p P p F p < 1 k 1 S k = 1 S k
166 5 ad3antrrr φ p P p F p < 1 k F A
167 ax-1ne0 1 0
168 1 qrng1 1 = 1 Q
169 2 168 22 abv1z F A 1 0 F 1 = 1
170 166 167 169 sylancl φ p P p F p < 1 k F 1 = 1
171 15 ad2antrr φ p P p F p < 1 P
172 nnnn0 k k 0
173 nnexpcl P k 0 P k
174 171 172 173 syl2an φ p P p F p < 1 k P k
175 174 nnzd φ p P p F p < 1 k P k
176 102 ad2antlr φ p P p F p < 1 p
177 nnexpcl p k 0 p k
178 176 172 177 syl2an φ p P p F p < 1 k p k
179 178 nnzd φ p P p F p < 1 k p k
180 bezout P k p k a b P k gcd p k = P k a + p k b
181 175 179 180 syl2anc φ p P p F p < 1 k a b P k gcd p k = P k a + p k b
182 simprl φ p P p F p < 1 P p
183 7 ad2antrr φ p P p F p < 1 P
184 simplr φ p P p F p < 1 p
185 prmrp P p P gcd p = 1 P p
186 183 184 185 syl2anc φ p P p F p < 1 P gcd p = 1 P p
187 182 186 mpbird φ p P p F p < 1 P gcd p = 1
188 187 adantr φ p P p F p < 1 k P gcd p = 1
189 171 adantr φ p P p F p < 1 k P
190 176 adantr φ p P p F p < 1 k p
191 simpr φ p P p F p < 1 k k
192 rppwr P p k P gcd p = 1 P k gcd p k = 1
193 189 190 191 192 syl3anc φ p P p F p < 1 k P gcd p = 1 P k gcd p k = 1
194 188 193 mpd φ p P p F p < 1 k P k gcd p k = 1
195 194 adantrr φ p P p F p < 1 k a b P k gcd p k = 1
196 195 eqeq1d φ p P p F p < 1 k a b P k gcd p k = P k a + p k b 1 = P k a + p k b
197 5 ad3antrrr φ p P p F p < 1 k a b F A
198 174 adantrr φ p P p F p < 1 k a b P k
199 nnq P k P k
200 198 199 syl φ p P p F p < 1 k a b P k
201 simprrl φ p P p F p < 1 k a b a
202 zq a a
203 201 202 syl φ p P p F p < 1 k a b a
204 qmulcl P k a P k a
205 200 203 204 syl2anc φ p P p F p < 1 k a b P k a
206 178 adantrr φ p P p F p < 1 k a b p k
207 nnq p k p k
208 206 207 syl φ p P p F p < 1 k a b p k
209 simprrr φ p P p F p < 1 k a b b
210 zq b b
211 209 210 syl φ p P p F p < 1 k a b b
212 qmulcl p k b p k b
213 208 211 212 syl2anc φ p P p F p < 1 k a b p k b
214 qaddcl P k a p k b P k a + p k b
215 205 213 214 syl2anc φ p P p F p < 1 k a b P k a + p k b
216 2 18 abvcl F A P k a + p k b F P k a + p k b
217 197 215 216 syl2anc φ p P p F p < 1 k a b F P k a + p k b
218 2 18 abvcl F A P k a F P k a
219 197 205 218 syl2anc φ p P p F p < 1 k a b F P k a
220 2 18 abvcl F A p k b F p k b
221 197 213 220 syl2anc φ p P p F p < 1 k a b F p k b
222 219 221 readdcld φ p P p F p < 1 k a b F P k a + F p k b
223 rpexpcl S + k S k +
224 146 163 223 syl2an φ p P p F p < 1 k S k +
225 224 rpred φ p P p F p < 1 k S k
226 225 adantrr φ p P p F p < 1 k a b S k
227 remulcl 2 S k 2 S k
228 135 226 227 sylancr φ p P p F p < 1 k a b 2 S k
229 qex V
230 cnfldadd + = + fld
231 1 230 ressplusg V + = + Q
232 229 231 ax-mp + = + Q
233 2 18 232 abvtri F A P k a p k b F P k a + p k b F P k a + F p k b
234 197 205 213 233 syl3anc φ p P p F p < 1 k a b F P k a + p k b F P k a + F p k b
235 cnfldmul × = fld
236 1 235 ressmulr V × = Q
237 229 236 ax-mp × = Q
238 2 18 237 abvmul F A P k a F P k a = F P k F a
239 197 200 203 238 syl3anc φ p P p F p < 1 k a b F P k a = F P k F a
240 17 ad3antrrr φ p P p F p < 1 k a b P
241 172 ad2antrl φ p P p F p < 1 k a b k 0
242 1 2 qabvexp F A P k 0 F P k = F P k
243 197 240 241 242 syl3anc φ p P p F p < 1 k a b F P k = F P k
244 243 oveq1d φ p P p F p < 1 k a b F P k F a = F P k F a
245 239 244 eqtrd φ p P p F p < 1 k a b F P k a = F P k F a
246 197 240 19 syl2anc φ p P p F p < 1 k a b F P
247 246 241 reexpcld φ p P p F p < 1 k a b F P k
248 2 18 abvcl F A a F a
249 197 203 248 syl2anc φ p P p F p < 1 k a b F a
250 247 249 remulcld φ p P p F p < 1 k a b F P k F a
251 elz a a a = 0 a a
252 251 simprbi a a = 0 a a
253 252 adantl φ a a = 0 a a
254 2 22 abv0 F A F 0 = 0
255 5 254 syl φ F 0 = 0
256 0le1 0 1
257 255 256 eqbrtrdi φ F 0 1
258 257 adantr φ a F 0 1
259 fveq2 a = 0 F a = F 0
260 259 breq1d a = 0 F a 1 F 0 1
261 258 260 syl5ibrcom φ a a = 0 F a 1
262 nnq n n
263 2 18 abvcl F A n F n
264 5 262 263 syl2an φ n F n
265 1re 1
266 lenlt F n 1 F n 1 ¬ 1 < F n
267 264 265 266 sylancl φ n F n 1 ¬ 1 < F n
268 267 ralbidva φ n F n 1 n ¬ 1 < F n
269 6 268 mpbird φ n F n 1
270 fveq2 n = a F n = F a
271 270 breq1d n = a F n 1 F a 1
272 271 rspccv n F n 1 a F a 1
273 269 272 syl φ a F a 1
274 273 adantr φ a a F a 1
275 5 adantr φ a a F A
276 202 ad2antrl φ a a a
277 eqid inv g Q = inv g Q
278 2 18 277 abvneg F A a F inv g Q a = F a
279 275 276 278 syl2anc φ a a F inv g Q a = F a
280 fveq2 n = inv g Q a F n = F inv g Q a
281 280 breq1d n = inv g Q a F n 1 F inv g Q a 1
282 269 adantr φ a a n F n 1
283 1 qrngneg a inv g Q a = a
284 276 283 syl φ a a inv g Q a = a
285 simprr φ a a a
286 284 285 eqeltrd φ a a inv g Q a
287 281 282 286 rspcdva φ a a F inv g Q a 1
288 279 287 eqbrtrrd φ a a F a 1
289 288 expr φ a a F a 1
290 261 274 289 3jaod φ a a = 0 a a F a 1
291 253 290 mpd φ a F a 1
292 291 ralrimiva φ a F a 1
293 292 ad3antrrr φ p P p F p < 1 k a b a F a 1
294 rsp a F a 1 a F a 1
295 293 201 294 sylc φ p P p F p < 1 k a b F a 1
296 265 a1i φ p P p F p < 1 k a b 1
297 163 ad2antrl φ p P p F p < 1 k a b k
298 24 ad3antrrr φ p P p F p < 1 k a b 0 < F P
299 expgt0 F P k 0 < F P 0 < F P k
300 246 297 298 299 syl3anc φ p P p F p < 1 k a b 0 < F P k
301 lemul2 F a 1 F P k 0 < F P k F a 1 F P k F a F P k 1
302 249 296 247 300 301 syl112anc φ p P p F p < 1 k a b F a 1 F P k F a F P k 1
303 295 302 mpbid φ p P p F p < 1 k a b F P k F a F P k 1
304 247 recnd φ p P p F p < 1 k a b F P k
305 304 mulid1d φ p P p F p < 1 k a b F P k 1 = F P k
306 303 305 breqtrd φ p P p F p < 1 k a b F P k F a F P k
307 146 rpred φ p P p F p < 1 S
308 307 adantr φ p P p F p < 1 k a b S
309 144 adantr φ p P p F p < 1 k a b F P +
310 309 rpge0d φ p P p F p < 1 k a b 0 F P
311 176 adantr φ p P p F p < 1 k a b p
312 311 104 syl φ p P p F p < 1 k a b p
313 197 312 138 syl2anc φ p P p F p < 1 k a b F p
314 max1 F P F p F P if F P F p F p F P
315 246 313 314 syl2anc φ p P p F p < 1 k a b F P if F P F p F p F P
316 315 10 breqtrrdi φ p P p F p < 1 k a b F P S
317 leexp1a F P S k 0 0 F P F P S F P k S k
318 246 308 241 310 316 317 syl32anc φ p P p F p < 1 k a b F P k S k
319 250 247 226 306 318 letrd φ p P p F p < 1 k a b F P k F a S k
320 245 319 eqbrtrd φ p P p F p < 1 k a b F P k a S k
321 2 18 237 abvmul F A p k b F p k b = F p k F b
322 197 208 211 321 syl3anc φ p P p F p < 1 k a b F p k b = F p k F b
323 1 2 qabvexp F A p k 0 F p k = F p k
324 197 312 241 323 syl3anc φ p P p F p < 1 k a b F p k = F p k
325 324 oveq1d φ p P p F p < 1 k a b F p k F b = F p k F b
326 322 325 eqtrd φ p P p F p < 1 k a b F p k b = F p k F b
327 313 241 reexpcld φ p P p F p < 1 k a b F p k
328 2 18 abvcl F A b F b
329 197 211 328 syl2anc φ p P p F p < 1 k a b F b
330 327 329 remulcld φ p P p F p < 1 k a b F p k F b
331 fveq2 a = b F a = F b
332 331 breq1d a = b F a 1 F b 1
333 332 293 209 rspcdva φ p P p F p < 1 k a b F b 1
334 311 nnne0d φ p P p F p < 1 k a b p 0
335 197 312 334 140 syl3anc φ p P p F p < 1 k a b 0 < F p
336 expgt0 F p k 0 < F p 0 < F p k
337 313 297 335 336 syl3anc φ p P p F p < 1 k a b 0 < F p k
338 lemul2 F b 1 F p k 0 < F p k F b 1 F p k F b F p k 1
339 329 296 327 337 338 syl112anc φ p P p F p < 1 k a b F b 1 F p k F b F p k 1
340 333 339 mpbid φ p P p F p < 1 k a b F p k F b F p k 1
341 327 recnd φ p P p F p < 1 k a b F p k
342 341 mulid1d φ p P p F p < 1 k a b F p k 1 = F p k
343 340 342 breqtrd φ p P p F p < 1 k a b F p k F b F p k
344 143 adantr φ p P p F p < 1 k a b F p +
345 344 rpge0d φ p P p F p < 1 k a b 0 F p
346 max2 F P F p F p if F P F p F p F P
347 246 313 346 syl2anc φ p P p F p < 1 k a b F p if F P F p F p F P
348 347 10 breqtrrdi φ p P p F p < 1 k a b F p S
349 leexp1a F p S k 0 0 F p F p S F p k S k
350 313 308 241 345 348 349 syl32anc φ p P p F p < 1 k a b F p k S k
351 330 327 226 343 350 letrd φ p P p F p < 1 k a b F p k F b S k
352 326 351 eqbrtrd φ p P p F p < 1 k a b F p k b S k
353 219 221 226 226 320 352 le2addd φ p P p F p < 1 k a b F P k a + F p k b S k + S k
354 224 rpcnd φ p P p F p < 1 k S k
355 354 2timesd φ p P p F p < 1 k 2 S k = S k + S k
356 355 adantrr φ p P p F p < 1 k a b 2 S k = S k + S k
357 353 356 breqtrrd φ p P p F p < 1 k a b F P k a + F p k b 2 S k
358 217 222 228 234 357 letrd φ p P p F p < 1 k a b F P k a + p k b 2 S k
359 fveq2 1 = P k a + p k b F 1 = F P k a + p k b
360 359 breq1d 1 = P k a + p k b F 1 2 S k F P k a + p k b 2 S k
361 358 360 syl5ibrcom φ p P p F p < 1 k a b 1 = P k a + p k b F 1 2 S k
362 196 361 sylbid φ p P p F p < 1 k a b P k gcd p k = P k a + p k b F 1 2 S k
363 362 anassrs φ p P p F p < 1 k a b P k gcd p k = P k a + p k b F 1 2 S k
364 363 rexlimdvva φ p P p F p < 1 k a b P k gcd p k = P k a + p k b F 1 2 S k
365 181 364 mpd φ p P p F p < 1 k F 1 2 S k
366 170 365 eqbrtrrd φ p P p F p < 1 k 1 2 S k
367 224 rpregt0d φ p P p F p < 1 k S k 0 < S k
368 ledivmul2 1 2 S k 0 < S k 1 S k 2 1 2 S k
369 265 135 367 368 mp3an12i φ p P p F p < 1 k 1 S k 2 1 2 S k
370 366 369 mpbird φ p P p F p < 1 k 1 S k 2
371 165 370 eqbrtrd φ p P p F p < 1 k 1 S k 2
372 reexpcl 1 S k 0 1 S k
373 147 172 372 syl2an φ p P p F p < 1 k 1 S k
374 lenlt 1 S k 2 1 S k 2 ¬ 2 < 1 S k
375 373 135 374 sylancl φ p P p F p < 1 k 1 S k 2 ¬ 2 < 1 S k
376 371 375 mpbid φ p P p F p < 1 k ¬ 2 < 1 S k
377 376 pm2.21d φ p P p F p < 1 k 2 < 1 S k ¬ F p < 1
378 377 rexlimdva φ p P p F p < 1 k 2 < 1 S k ¬ F p < 1
379 158 378 mpd φ p P p F p < 1 ¬ F p < 1
380 379 expr φ p P p F p < 1 ¬ F p < 1
381 380 pm2.01d φ p P p ¬ F p < 1
382 fveq2 n = p F n = F p
383 382 breq2d n = p 1 < F n 1 < F p
384 383 notbid n = p ¬ 1 < F n ¬ 1 < F p
385 6 ad2antrr φ p P p n ¬ 1 < F n
386 384 385 103 rspcdva φ p P p ¬ 1 < F p
387 lttri3 F p 1 F p = 1 ¬ F p < 1 ¬ 1 < F p
388 139 265 387 sylancl φ p P p F p = 1 ¬ F p < 1 ¬ 1 < F p
389 381 386 388 mpbir2and φ p P p F p = 1
390 112 134 389 3eqtr4d φ p P p J P p R = F p
391 110 390 eqtr2d φ p P p F p = y J P y R p
392 391 ex φ p P p F p = y J P y R p
393 101 392 pm2.61dne φ p F p = y J P y R p
394 1 2 5 50 393 ostthlem2 φ F = y J P y R
395 oveq2 a = R J P y a = J P y R
396 395 mpteq2dv a = R y J P y a = y J P y R
397 396 rspceeqv R + F = y J P y R a + F = y J P y a
398 48 394 397 syl2anc φ a + F = y J P y a