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

Theorem sylow1lem1 15187
 Description: Lemma for sylow1 15192. The p-adic valuation of the size of is equal to the number of excess powers of in . (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x
sylow1.g
sylow1.f
sylow1.p
sylow1.n
sylow1.d
sylow1lem.a
sylow1lem.s
Assertion
Ref Expression
sylow1lem1
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem sylow1lem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1.f . . . . 5
2 sylow1.p . . . . . . . 8
3 prmnn 13037 . . . . . . . 8
42, 3syl 16 . . . . . . 7
5 sylow1.n . . . . . . 7
64, 5nnexpcld 11499 . . . . . 6
76nnzd 10330 . . . . 5
8 hashbc 11657 . . . . 5
91, 7, 8syl2anc 643 . . . 4
10 sylow1lem.s . . . . 5
1110fveq2i 5690 . . . 4
129, 11syl6eqr 2454 . . 3
13 sylow1.d . . . . . 6
14 sylow1.g . . . . . . . . . 10
15 sylow1.x . . . . . . . . . . 11
1615grpbn0 14789 . . . . . . . . . 10
1714, 16syl 16 . . . . . . . . 9
18 hasheq0 11599 . . . . . . . . . . 11
191, 18syl 16 . . . . . . . . . 10
2019necon3bbid 2601 . . . . . . . . 9
2117, 20mpbird 224 . . . . . . . 8
22 hashcl 11594 . . . . . . . . . . 11
231, 22syl 16 . . . . . . . . . 10
24 elnn0 10179 . . . . . . . . . 10
2523, 24sylib 189 . . . . . . . . 9
2625ord 367 . . . . . . . 8
2721, 26mt3d 119 . . . . . . 7
28 dvdsle 12850 . . . . . . 7
297, 27, 28syl2anc 643 . . . . . 6
3013, 29mpd 15 . . . . 5
316nnnn0d 10230 . . . . . . 7
32 nn0uz 10476 . . . . . . 7
3331, 32syl6eleq 2494 . . . . . 6
3423nn0zd 10329 . . . . . 6
35 elfz5 11007 . . . . . 6
3633, 34, 35syl2anc 643 . . . . 5
3730, 36mpbird 224 . . . 4
38 bccl2 11569 . . . 4
3937, 38syl 16 . . 3
4012, 39eqeltrrd 2479 . 2
41 nnuz 10477 . . . . . . . . . . 11
426, 41syl6eleq 2494 . . . . . . . . . 10
43 elfz5 11007 . . . . . . . . . 10
4442, 34, 43syl2anc 643 . . . . . . . . 9
4530, 44mpbird 224 . . . . . . . 8
46 1z 10267 . . . . . . . . . 10
4746a1i 11 . . . . . . . . 9
48 fzsubel 11044 . . . . . . . . 9
4947, 34, 7, 47, 48syl22anc 1185 . . . . . . . 8
5045, 49mpbid 202 . . . . . . 7
51 1m1e0 10024 . . . . . . . 8
5251oveq1i 6050 . . . . . . 7
5350, 52syl6eleq 2494 . . . . . 6
54 bcp1nk 11563 . . . . . 6
5553, 54syl 16 . . . . 5
5623nn0cnd 10232 . . . . . . 7
57 ax-1cn 9004 . . . . . . 7
58 npcan 9270 . . . . . . 7
5956, 57, 58sylancl 644 . . . . . 6
606nncnd 9972 . . . . . . 7
61 npcan 9270 . . . . . . 7
6260, 57, 61sylancl 644 . . . . . 6
6359, 62oveq12d 6058 . . . . 5
6459, 62oveq12d 6058 . . . . . 6
6564oveq2d 6056 . . . . 5
6655, 63, 653eqtr3d 2444 . . . 4
6766oveq2d 6056 . . 3
6812oveq2d 6056 . . 3
69 bccl2 11569 . . . . . . 7
7053, 69syl 16 . . . . . 6
7170nnzd 10330 . . . . 5
7270nnne0d 10000 . . . . 5
736nnne0d 10000 . . . . . . 7
74 dvdsval2 12810 . . . . . . 7
757, 73, 34, 74syl3anc 1184 . . . . . 6
7613, 75mpbid 202 . . . . 5
7727nnne0d 10000 . . . . . 6
7856, 60, 77, 73divne0d 9762 . . . . 5
79 pcmul 13180 . . . . 5
802, 71, 72, 76, 78, 79syl122anc 1193 . . . 4
8157a1i 11 . . . . . . . . 9
8256, 60, 81npncand 9391 . . . . . . . 8
8382oveq1d 6055 . . . . . . 7
8483oveq2d 6056 . . . . . 6
856nnred 9971 . . . . . . . 8
8685ltm1d 9899 . . . . . . 7
87 nnm1nn0 10217 . . . . . . . . 9
886, 87syl 16 . . . . . . . 8
89 breq1 4175 . . . . . . . . . . 11
90 bcxmaslem1 12568 . . . . . . . . . . . . 13
9190oveq2d 6056 . . . . . . . . . . . 12
9291eqeq1d 2412 . . . . . . . . . . 11
9389, 92imbi12d 312 . . . . . . . . . 10
9493imbi2d 308 . . . . . . . . 9
95 breq1 4175 . . . . . . . . . . 11
96 bcxmaslem1 12568 . . . . . . . . . . . . 13
9796oveq2d 6056 . . . . . . . . . . . 12
9897eqeq1d 2412 . . . . . . . . . . 11
9995, 98imbi12d 312 . . . . . . . . . 10
10099imbi2d 308 . . . . . . . . 9
101 breq1 4175 . . . . . . . . . . 11
102 bcxmaslem1 12568 . . . . . . . . . . . . 13
103102oveq2d 6056 . . . . . . . . . . . 12
104103eqeq1d 2412 . . . . . . . . . . 11
105101, 104imbi12d 312 . . . . . . . . . 10
106105imbi2d 308 . . . . . . . . 9
107 breq1 4175 . . . . . . . . . . 11
108 bcxmaslem1 12568 . . . . . . . . . . . . 13
109108oveq2d 6056 . . . . . . . . . . . 12
110109eqeq1d 2412 . . . . . . . . . . 11
111107, 110imbi12d 312 . . . . . . . . . 10
112111imbi2d 308 . . . . . . . . 9
113 znn0sub 10279 . . . . . . . . . . . . . . . 16
1147, 34, 113syl2anc 643 . . . . . . . . . . . . . . 15
11530, 114mpbid 202 . . . . . . . . . . . . . 14
116 0nn0 10192 . . . . . . . . . . . . . 14
117 nn0addcl 10211 . . . . . . . . . . . . . 14
118115, 116, 117sylancl 644 . . . . . . . . . . . . 13
119 bcn0 11556 . . . . . . . . . . . . 13
120118, 119syl 16 . . . . . . . . . . . 12
121120oveq2d 6056 . . . . . . . . . . 11
122 pc1 13184 . . . . . . . . . . . 12
1232, 122syl 16 . . . . . . . . . . 11
124121, 123eqtrd 2436 . . . . . . . . . 10
125124a1d 23 . . . . . . . . 9
126 nn0re 10186 . . . . . . . . . . . . . . . 16
127126ad2antrl 709 . . . . . . . . . . . . . . 15
128 nn0p1nn 10215 . . . . . . . . . . . . . . . . 17
129128ad2antrl 709 . . . . . . . . . . . . . . . 16
130129nnred 9971 . . . . . . . . . . . . . . 15
1316adantr 452 . . . . . . . . . . . . . . . 16
132131nnred 9971 . . . . . . . . . . . . . . 15
133127ltp1d 9897 . . . . . . . . . . . . . . 15
134 simprr 734 . . . . . . . . . . . . . . 15
135127, 130, 132, 133, 134lttrd 9187 . . . . . . . . . . . . . 14
136135expr 599 . . . . . . . . . . . . 13
137136imim1d 71 . . . . . . . . . . . 12
138 oveq1 6047 . . . . . . . . . . . . . . 15
139115adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
140139nn0cnd 10232 . . . . . . . . . . . . . . . . . . . . 21
141 nn0cn 10187 . . . . . . . . . . . . . . . . . . . . . 22
142141ad2antrl 709 . . . . . . . . . . . . . . . . . . . . 21
14357a1i 11 . . . . . . . . . . . . . . . . . . . . 21
144140, 142, 143addassd 9066 . . . . . . . . . . . . . . . . . . . 20
145144oveq1d 6055 . . . . . . . . . . . . . . . . . . 19
146 nn0addge2 10223 . . . . . . . . . . . . . . . . . . . . . 22
147127, 139, 146syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
148 simprl 733 . . . . . . . . . . . . . . . . . . . . . . 23
149148, 32syl6eleq 2494 . . . . . . . . . . . . . . . . . . . . . 22
150139, 148nn0addcld 10234 . . . . . . . . . . . . . . . . . . . . . . 23
151150nn0zd 10329 . . . . . . . . . . . . . . . . . . . . . 22
152 elfz5 11007 . . . . . . . . . . . . . . . . . . . . . 22
153149, 151, 152syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
154147, 153mpbird 224 . . . . . . . . . . . . . . . . . . . 20
155 bcp1nk 11563 . . . . . . . . . . . . . . . . . . . 20
156154, 155syl 16 . . . . . . . . . . . . . . . . . . 19
157145, 156eqtr3d 2438 . . . . . . . . . . . . . . . . . 18
158157oveq2d 6056 . . . . . . . . . . . . . . . . 17
1592adantr 452 . . . . . . . . . . . . . . . . . 18
160 bccl2 11569 . . . . . . . . . . . . . . . . . . . 20
161154, 160syl 16 . . . . . . . . . . . . . . . . . . 19
162 nnq 10543 . . . . . . . . . . . . . . . . . . 19
163161, 162syl 16 . . . . . . . . . . . . . . . . . 18
164161nnne0d 10000 . . . . . . . . . . . . . . . . . 18
165151peano2zd 10334 . . . . . . . . . . . . . . . . . . 19
166 znq 10534 . . . . . . . . . . . . . . . . . . 19
167165, 129, 166syl2anc 643 . . . . . . . . . . . . . . . . . 18
168 nn0p1nn 10215 . . . . . . . . . . . . . . . . . . . . 21
169150, 168syl 16 . . . . . . . . . . . . . . . . . . . 20
170 nnrp 10577 . . . . . . . . . . . . . . . . . . . . 21
171 nnrp 10577 . . . . . . . . . . . . . . . . . . . . 21
172 rpdivcl 10590 . . . . . . . . . . . . . . . . . . . . 21
173170, 171, 172syl2an 464 . . . . . . . . . . . . . . . . . . . 20
174169, 129, 173syl2anc 643 . . . . . . . . . . . . . . . . . . 19
175174rpne0d 10609 . . . . . . . . . . . . . . . . . 18
176 pcqmul 13182 . . . . . . . . . . . . . . . . . 18
177159, 163, 164, 167, 175, 176syl122anc 1193 . . . . . . . . . . . . . . . . 17
178158, 177eqtrd 2436 . . . . . . . . . . . . . . . 16
179169nnne0d 10000 . . . . . . . . . . . . . . . . . . . 20
180 pcdiv 13181 . . . . . . . . . . . . . . . . . . . 20
181159, 165, 179, 129, 180syl121anc 1189 . . . . . . . . . . . . . . . . . . 19
182129nncnd 9972 . . . . . . . . . . . . . . . . . . . . . . . . 25
183140, 182addcomd 9224 . . . . . . . . . . . . . . . . . . . . . . . 24
184144, 183eqtrd 2436 . . . . . . . . . . . . . . . . . . . . . . 23
185184oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . 22
186 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26
187186oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . . . 25
188182addid1d 9222 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189188adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
190187, 189eqtr2d 2437 . . . . . . . . . . . . . . . . . . . . . . . 24
191190oveq2d 6056 . . . . . . . . . . . . . . . . . . . . . . 23
1922ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
193 nnq 10543 . . . . . . . . . . . . . . . . . . . . . . . . . 26
194129, 193syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
195194adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
196139nn0zd 10329 . . . . . . . . . . . . . . . . . . . . . . . . . 26
197 zq 10536 . . . . . . . . . . . . . . . . . . . . . . . . . 26
198196, 197syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
199198adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24
200159, 129pccld 13179 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
201200nn0red 10231 . . . . . . . . . . . . . . . . . . . . . . . . . 26
202201adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
2035adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
204203nn0red 10231 . . . . . . . . . . . . . . . . . . . . . . . . . 26
205204adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
206 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
207206neneqd 2583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
208115ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
209 elnn0 10179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
210208, 209sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
211210ord 367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
212207, 211mt3d 119 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
213192, 212pccld 13179 . . . . . . . . . . . . . . . . . . . . . . . . . 26
214213nn0red 10231 . . . . . . . . . . . . . . . . . . . . . . . . 25
215129nnzd 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
216 pcdvdsb 13197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
217159, 215, 203, 216syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2187adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
219 dvdsle 12850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
220218, 129, 219syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
221217, 220sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
222204, 201lenltd 9175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
223132, 130lenltd 9175 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
224221, 222, 2233imtr3d 259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
225134, 224mt4d 132 . . . . . . . . . . . . . . . . . . . . . . . . . 26
226225adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
227 dvdssubr 12846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2287, 34, 227syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
22913, 228mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
230229ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26
231208nn0zd 10329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2325ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
233 pcdvdsb 13197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
234192, 231, 232, 233syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26
235230, 234mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . 25
236202, 205, 214, 226, 235ltletrd 9186 . . . . . . . . . . . . . . . . . . . . . . . 24
237192, 195, 199, 236pcadd2 13214 . . . . . . . . . . . . . . . . . . . . . . 23
238191, 237pm2.61dane 2645 . . . . . . . . . . . . . . . . . . . . . 22
239185, 238eqtr4d 2439 . . . . . . . . . . . . . . . . . . . . 21
240200nn0cnd 10232 . . . . . . . . . . . . . . . . . . . . 21
241239, 240eqeltrd 2478 . . . . . . . . . . . . . . . . . . . 20
242241, 239subeq0bd 9419 . . . . . . . . . . . . . . . . . . 19
243181, 242eqtrd 2436 . . . . . . . . . . . . . . . . . 18
244243oveq2d 6056 . . . . . . . . . . . . . . . . 17
245 00id 9197 . . . . . . . . . . . . . . . . 17
246244, 245syl6req 2453 . . . . . . . . . . . . . . . 16
247178, 246eqeq12d 2418 . . . . . . . . . . . . . . 15
248138, 247syl5ibr 213 . . . . . . . . . . . . . 14
249248expr 599 . . . . . . . . . . . . 13
250249a2d 24 . . . . . . . . . . . 12
251137, 250syld 42 . . . . . . . . . . 11
252251expcom 425 . . . . . . . . . 10
253252a2d 24 . . . . . . . . 9
25494, 100, 106, 112, 125, 253nn0ind 10322 . . . . . . . 8
25588, 254mpcom 34 . . . . . . 7
25686, 255mpd 15 . . . . . 6
25784, 256eqtr3d 2438 . . . . 5
258 pcdiv 13181 . . . . . . 7
2592, 34, 77, 6, 258syl121anc 1189 . . . . . 6
2605nn0zd 10329 . . . . . . . 8
261 pcid 13201 . . . . . . . 8
2622, 260, 261syl2anc 643 . . . . . . 7
263262oveq2d 6056 . . . . . 6
264259, 263eqtrd 2436 . . . . 5
265257, 264oveq12d 6058 . . . 4
2662, 27pccld 13179 . . . . . . . 8
267266nn0zd 10329 . . . . . . 7
268267, 260zsubcld 10336 . . . . . 6
269268zcnd 10332 . . . . 5
270269addid2d 9223 . . . 4
27180, 265, 2703eqtrd 2440 . . 3
27267, 68, 2713eqtr3d 2444 . 2
27340, 272jca 519 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2567  crab 2670  c0 3588  cpw 3759   class class class wbr 4172  cfv 5413  (class class class)co 6040  cfn 7068  cc 8944  cr 8945  cc0 8946  c1 8947   caddc 8949   cmul 8951   clt 9076   cle 9077   cmin 9247   cdiv 9633  cn 9956  cn0 10177  cz 10238  cuz 10444  cq 10530  crp 10568  cfz 10999  cexp 11337   cbc 11548  chash 11573   cdivides 12807  cprime 13034   cpc 13165  cbs 13424   cplusg 13484  cgrp 14640 This theorem is referenced by:  sylow1lem3  15189 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-fz 11000  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-dvds 12808  df-gcd 12962  df-prm 13035  df-pc 13166  df-0g 13682  df-mnd 14645  df-grp 14767
 Copyright terms: Public domain W3C validator