Metamath Proof Explorer


Theorem sylow1lem1

Description: Lemma for sylow1 . The p-adic valuation of the size of S is equal to the number of excess powers of P in ( #X ) / ( P ^ N ) . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses sylow1.x X = Base G
sylow1.g φ G Grp
sylow1.f φ X Fin
sylow1.p φ P
sylow1.n φ N 0
sylow1.d φ P N X
sylow1lem.a + ˙ = + G
sylow1lem.s S = s 𝒫 X | s = P N
Assertion sylow1lem1 φ S P pCnt S = P pCnt X N

Proof

Step Hyp Ref Expression
1 sylow1.x X = Base G
2 sylow1.g φ G Grp
3 sylow1.f φ X Fin
4 sylow1.p φ P
5 sylow1.n φ N 0
6 sylow1.d φ P N X
7 sylow1lem.a + ˙ = + G
8 sylow1lem.s S = s 𝒫 X | s = P N
9 prmnn P P
10 4 9 syl φ P
11 10 5 nnexpcld φ P N
12 11 nnzd φ P N
13 hashbc X Fin P N ( X P N ) = s 𝒫 X | s = P N
14 3 12 13 syl2anc φ ( X P N ) = s 𝒫 X | s = P N
15 8 fveq2i S = s 𝒫 X | s = P N
16 14 15 eqtr4di φ ( X P N ) = S
17 1 grpbn0 G Grp X
18 2 17 syl φ X
19 hasheq0 X Fin X = 0 X =
20 3 19 syl φ X = 0 X =
21 20 necon3bbid φ ¬ X = 0 X
22 18 21 mpbird φ ¬ X = 0
23 hashcl X Fin X 0
24 3 23 syl φ X 0
25 elnn0 X 0 X X = 0
26 24 25 sylib φ X X = 0
27 26 ord φ ¬ X X = 0
28 22 27 mt3d φ X
29 dvdsle P N X P N X P N X
30 12 28 29 syl2anc φ P N X P N X
31 6 30 mpd φ P N X
32 11 nnnn0d φ P N 0
33 nn0uz 0 = 0
34 32 33 eleqtrdi φ P N 0
35 24 nn0zd φ X
36 elfz5 P N 0 X P N 0 X P N X
37 34 35 36 syl2anc φ P N 0 X P N X
38 31 37 mpbird φ P N 0 X
39 bccl2 P N 0 X ( X P N )
40 38 39 syl φ ( X P N )
41 16 40 eqeltrrd φ S
42 nnuz = 1
43 11 42 eleqtrdi φ P N 1
44 elfz5 P N 1 X P N 1 X P N X
45 43 35 44 syl2anc φ P N 1 X P N X
46 31 45 mpbird φ P N 1 X
47 1zzd φ 1
48 fzsubel 1 X P N 1 P N 1 X P N 1 1 1 X 1
49 47 35 12 47 48 syl22anc φ P N 1 X P N 1 1 1 X 1
50 46 49 mpbid φ P N 1 1 1 X 1
51 1m1e0 1 1 = 0
52 51 oveq1i 1 1 X 1 = 0 X 1
53 50 52 eleqtrdi φ P N 1 0 X 1
54 bcp1nk P N 1 0 X 1 ( X - 1 + 1 P N - 1 + 1 ) = ( X 1 P N 1 ) X - 1 + 1 P N - 1 + 1
55 53 54 syl φ ( X - 1 + 1 P N - 1 + 1 ) = ( X 1 P N 1 ) X - 1 + 1 P N - 1 + 1
56 24 nn0cnd φ X
57 ax-1cn 1
58 npcan X 1 X - 1 + 1 = X
59 56 57 58 sylancl φ X - 1 + 1 = X
60 11 nncnd φ P N
61 npcan P N 1 P N - 1 + 1 = P N
62 60 57 61 sylancl φ P N - 1 + 1 = P N
63 59 62 oveq12d φ ( X - 1 + 1 P N - 1 + 1 ) = ( X P N )
64 59 62 oveq12d φ X - 1 + 1 P N - 1 + 1 = X P N
65 64 oveq2d φ ( X 1 P N 1 ) X - 1 + 1 P N - 1 + 1 = ( X 1 P N 1 ) X P N
66 55 63 65 3eqtr3d φ ( X P N ) = ( X 1 P N 1 ) X P N
67 66 oveq2d φ P pCnt ( X P N ) = P pCnt ( X 1 P N 1 ) X P N
68 16 oveq2d φ P pCnt ( X P N ) = P pCnt S
69 bccl2 P N 1 0 X 1 ( X 1 P N 1 )
70 53 69 syl φ ( X 1 P N 1 )
71 70 nnzd φ ( X 1 P N 1 )
72 70 nnne0d φ ( X 1 P N 1 ) 0
73 11 nnne0d φ P N 0
74 dvdsval2 P N P N 0 X P N X X P N
75 12 73 35 74 syl3anc φ P N X X P N
76 6 75 mpbid φ X P N
77 28 nnne0d φ X 0
78 56 60 77 73 divne0d φ X P N 0
79 pcmul P ( X 1 P N 1 ) ( X 1 P N 1 ) 0 X P N X P N 0 P pCnt ( X 1 P N 1 ) X P N = P pCnt ( X 1 P N 1 ) + P pCnt X P N
80 4 71 72 76 78 79 syl122anc φ P pCnt ( X 1 P N 1 ) X P N = P pCnt ( X 1 P N 1 ) + P pCnt X P N
81 1cnd φ 1
82 56 60 81 npncand φ X P N + P N - 1 = X 1
83 82 oveq1d φ ( X P N + P N - 1 P N 1 ) = ( X 1 P N 1 )
84 83 oveq2d φ P pCnt ( X P N + P N - 1 P N 1 ) = P pCnt ( X 1 P N 1 )
85 11 nnred φ P N
86 85 ltm1d φ P N 1 < P N
87 nnm1nn0 P N P N 1 0
88 11 87 syl φ P N 1 0
89 breq1 x = 0 x < P N 0 < P N
90 bcxmaslem1 x = 0 ( X - P N + x x) = ( X - P N + 0 0 )
91 90 oveq2d x = 0 P pCnt ( X - P N + x x) = P pCnt ( X - P N + 0 0 )
92 91 eqeq1d x = 0 P pCnt ( X - P N + x x) = 0 P pCnt ( X - P N + 0 0 ) = 0
93 89 92 imbi12d x = 0 x < P N P pCnt ( X - P N + x x) = 0 0 < P N P pCnt ( X - P N + 0 0 ) = 0
94 93 imbi2d x = 0 φ x < P N P pCnt ( X - P N + x x) = 0 φ 0 < P N P pCnt ( X - P N + 0 0 ) = 0
95 breq1 x = n x < P N n < P N
96 bcxmaslem1 x = n ( X - P N + x x) = ( X - P N + n n)
97 96 oveq2d x = n P pCnt ( X - P N + x x) = P pCnt ( X - P N + n n)
98 97 eqeq1d x = n P pCnt ( X - P N + x x) = 0 P pCnt ( X - P N + n n) = 0
99 95 98 imbi12d x = n x < P N P pCnt ( X - P N + x x) = 0 n < P N P pCnt ( X - P N + n n) = 0
100 99 imbi2d x = n φ x < P N P pCnt ( X - P N + x x) = 0 φ n < P N P pCnt ( X - P N + n n) = 0
101 breq1 x = n + 1 x < P N n + 1 < P N
102 bcxmaslem1 x = n + 1 ( X - P N + x x) = ( X P N + n + 1 n + 1 )
103 102 oveq2d x = n + 1 P pCnt ( X - P N + x x) = P pCnt ( X P N + n + 1 n + 1 )
104 103 eqeq1d x = n + 1 P pCnt ( X - P N + x x) = 0 P pCnt ( X P N + n + 1 n + 1 ) = 0
105 101 104 imbi12d x = n + 1 x < P N P pCnt ( X - P N + x x) = 0 n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = 0
106 105 imbi2d x = n + 1 φ x < P N P pCnt ( X - P N + x x) = 0 φ n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = 0
107 breq1 x = P N 1 x < P N P N 1 < P N
108 bcxmaslem1 x = P N 1 ( X - P N + x x) = ( X P N + P N - 1 P N 1 )
109 108 oveq2d x = P N 1 P pCnt ( X - P N + x x) = P pCnt ( X P N + P N - 1 P N 1 )
110 109 eqeq1d x = P N 1 P pCnt ( X - P N + x x) = 0 P pCnt ( X P N + P N - 1 P N 1 ) = 0
111 107 110 imbi12d x = P N 1 x < P N P pCnt ( X - P N + x x) = 0 P N 1 < P N P pCnt ( X P N + P N - 1 P N 1 ) = 0
112 111 imbi2d x = P N 1 φ x < P N P pCnt ( X - P N + x x) = 0 φ P N 1 < P N P pCnt ( X P N + P N - 1 P N 1 ) = 0
113 znn0sub P N X P N X X P N 0
114 12 35 113 syl2anc φ P N X X P N 0
115 31 114 mpbid φ X P N 0
116 0nn0 0 0
117 nn0addcl X P N 0 0 0 X - P N + 0 0
118 115 116 117 sylancl φ X - P N + 0 0
119 bcn0 X - P N + 0 0 ( X - P N + 0 0 ) = 1
120 118 119 syl φ ( X - P N + 0 0 ) = 1
121 120 oveq2d φ P pCnt ( X - P N + 0 0 ) = P pCnt 1
122 pc1 P P pCnt 1 = 0
123 4 122 syl φ P pCnt 1 = 0
124 121 123 eqtrd φ P pCnt ( X - P N + 0 0 ) = 0
125 124 a1d φ 0 < P N P pCnt ( X - P N + 0 0 ) = 0
126 nn0re n 0 n
127 126 ad2antrl φ n 0 n + 1 < P N n
128 nn0p1nn n 0 n + 1
129 128 ad2antrl φ n 0 n + 1 < P N n + 1
130 129 nnred φ n 0 n + 1 < P N n + 1
131 11 adantr φ n 0 n + 1 < P N P N
132 131 nnred φ n 0 n + 1 < P N P N
133 127 ltp1d φ n 0 n + 1 < P N n < n + 1
134 simprr φ n 0 n + 1 < P N n + 1 < P N
135 127 130 132 133 134 lttrd φ n 0 n + 1 < P N n < P N
136 135 expr φ n 0 n + 1 < P N n < P N
137 136 imim1d φ n 0 n < P N P pCnt ( X - P N + n n) = 0 n + 1 < P N P pCnt ( X - P N + n n) = 0
138 oveq1 P pCnt ( X - P N + n n) = 0 P pCnt ( X - P N + n n) + P pCnt X P N + n + 1 n + 1 = 0 + P pCnt X P N + n + 1 n + 1
139 115 adantr φ n 0 n + 1 < P N X P N 0
140 139 nn0cnd φ n 0 n + 1 < P N X P N
141 nn0cn n 0 n
142 141 ad2antrl φ n 0 n + 1 < P N n
143 1cnd φ n 0 n + 1 < P N 1
144 140 142 143 addassd φ n 0 n + 1 < P N X P N + n + 1 = X P N + n + 1
145 144 oveq1d φ n 0 n + 1 < P N ( X P N + n + 1 n + 1 ) = ( X P N + n + 1 n + 1 )
146 nn0addge2 n X P N 0 n X - P N + n
147 127 139 146 syl2anc φ n 0 n + 1 < P N n X - P N + n
148 simprl φ n 0 n + 1 < P N n 0
149 148 33 eleqtrdi φ n 0 n + 1 < P N n 0
150 139 148 nn0addcld φ n 0 n + 1 < P N X - P N + n 0
151 150 nn0zd φ n 0 n + 1 < P N X - P N + n
152 elfz5 n 0 X - P N + n n 0 X - P N + n n X - P N + n
153 149 151 152 syl2anc φ n 0 n + 1 < P N n 0 X - P N + n n X - P N + n
154 147 153 mpbird φ n 0 n + 1 < P N n 0 X - P N + n
155 bcp1nk n 0 X - P N + n ( X P N + n + 1 n + 1 ) = ( X - P N + n n) X P N + n + 1 n + 1
156 154 155 syl φ n 0 n + 1 < P N ( X P N + n + 1 n + 1 ) = ( X - P N + n n) X P N + n + 1 n + 1
157 145 156 eqtr3d φ n 0 n + 1 < P N ( X P N + n + 1 n + 1 ) = ( X - P N + n n) X P N + n + 1 n + 1
158 157 oveq2d φ n 0 n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = P pCnt ( X - P N + n n) X P N + n + 1 n + 1
159 4 adantr φ n 0 n + 1 < P N P
160 bccl2 n 0 X - P N + n ( X - P N + n n)
161 154 160 syl φ n 0 n + 1 < P N ( X - P N + n n)
162 nnq ( X - P N + n n) ( X - P N + n n)
163 161 162 syl φ n 0 n + 1 < P N ( X - P N + n n)
164 161 nnne0d φ n 0 n + 1 < P N ( X - P N + n n) 0
165 151 peano2zd φ n 0 n + 1 < P N X P N + n + 1
166 znq X P N + n + 1 n + 1 X P N + n + 1 n + 1
167 165 129 166 syl2anc φ n 0 n + 1 < P N X P N + n + 1 n + 1
168 nn0p1nn X - P N + n 0 X P N + n + 1
169 150 168 syl φ n 0 n + 1 < P N X P N + n + 1
170 nnrp X P N + n + 1 X P N + n + 1 +
171 nnrp n + 1 n + 1 +
172 rpdivcl X P N + n + 1 + n + 1 + X P N + n + 1 n + 1 +
173 170 171 172 syl2an X P N + n + 1 n + 1 X P N + n + 1 n + 1 +
174 169 129 173 syl2anc φ n 0 n + 1 < P N X P N + n + 1 n + 1 +
175 174 rpne0d φ n 0 n + 1 < P N X P N + n + 1 n + 1 0
176 pcqmul P ( X - P N + n n) ( X - P N + n n) 0 X P N + n + 1 n + 1 X P N + n + 1 n + 1 0 P pCnt ( X - P N + n n) X P N + n + 1 n + 1 = P pCnt ( X - P N + n n) + P pCnt X P N + n + 1 n + 1
177 159 163 164 167 175 176 syl122anc φ n 0 n + 1 < P N P pCnt ( X - P N + n n) X P N + n + 1 n + 1 = P pCnt ( X - P N + n n) + P pCnt X P N + n + 1 n + 1
178 158 177 eqtrd φ n 0 n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = P pCnt ( X - P N + n n) + P pCnt X P N + n + 1 n + 1
179 169 nnne0d φ n 0 n + 1 < P N X P N + n + 1 0
180 pcdiv P X P N + n + 1 X P N + n + 1 0 n + 1 P pCnt X P N + n + 1 n + 1 = P pCnt X P N + n + 1 P pCnt n + 1
181 159 165 179 129 180 syl121anc φ n 0 n + 1 < P N P pCnt X P N + n + 1 n + 1 = P pCnt X P N + n + 1 P pCnt n + 1
182 129 nncnd φ n 0 n + 1 < P N n + 1
183 140 182 144 comraddd φ n 0 n + 1 < P N X P N + n + 1 = n + 1 + X P N
184 183 oveq2d φ n 0 n + 1 < P N P pCnt X P N + n + 1 = P pCnt n + 1 + X P N
185 simpr φ n 0 n + 1 < P N X P N = 0 X P N = 0
186 185 oveq2d φ n 0 n + 1 < P N X P N = 0 n + 1 + X P N = n + 1 + 0
187 182 addid1d φ n 0 n + 1 < P N n + 1 + 0 = n + 1
188 187 adantr φ n 0 n + 1 < P N X P N = 0 n + 1 + 0 = n + 1
189 186 188 eqtr2d φ n 0 n + 1 < P N X P N = 0 n + 1 = n + 1 + X P N
190 189 oveq2d φ n 0 n + 1 < P N X P N = 0 P pCnt n + 1 = P pCnt n + 1 + X P N
191 4 ad2antrr φ n 0 n + 1 < P N X P N 0 P
192 nnq n + 1 n + 1
193 129 192 syl φ n 0 n + 1 < P N n + 1
194 193 adantr φ n 0 n + 1 < P N X P N 0 n + 1
195 139 nn0zd φ n 0 n + 1 < P N X P N
196 zq X P N X P N
197 195 196 syl φ n 0 n + 1 < P N X P N
198 197 adantr φ n 0 n + 1 < P N X P N 0 X P N
199 159 129 pccld φ n 0 n + 1 < P N P pCnt n + 1 0
200 199 nn0red φ n 0 n + 1 < P N P pCnt n + 1
201 200 adantr φ n 0 n + 1 < P N X P N 0 P pCnt n + 1
202 5 adantr φ n 0 n + 1 < P N N 0
203 202 nn0red φ n 0 n + 1 < P N N
204 203 adantr φ n 0 n + 1 < P N X P N 0 N
205 simpr φ n 0 n + 1 < P N X P N 0 X P N 0
206 205 neneqd φ n 0 n + 1 < P N X P N 0 ¬ X P N = 0
207 115 ad2antrr φ n 0 n + 1 < P N X P N 0 X P N 0
208 elnn0 X P N 0 X P N X P N = 0
209 207 208 sylib φ n 0 n + 1 < P N X P N 0 X P N X P N = 0
210 209 ord φ n 0 n + 1 < P N X P N 0 ¬ X P N X P N = 0
211 206 210 mt3d φ n 0 n + 1 < P N X P N 0 X P N
212 191 211 pccld φ n 0 n + 1 < P N X P N 0 P pCnt X P N 0
213 212 nn0red φ n 0 n + 1 < P N X P N 0 P pCnt X P N
214 129 nnzd φ n 0 n + 1 < P N n + 1
215 pcdvdsb P n + 1 N 0 N P pCnt n + 1 P N n + 1
216 159 214 202 215 syl3anc φ n 0 n + 1 < P N N P pCnt n + 1 P N n + 1
217 12 adantr φ n 0 n + 1 < P N P N
218 dvdsle P N n + 1 P N n + 1 P N n + 1
219 217 129 218 syl2anc φ n 0 n + 1 < P N P N n + 1 P N n + 1
220 216 219 sylbid φ n 0 n + 1 < P N N P pCnt n + 1 P N n + 1
221 203 200 lenltd φ n 0 n + 1 < P N N P pCnt n + 1 ¬ P pCnt n + 1 < N
222 132 130 lenltd φ n 0 n + 1 < P N P N n + 1 ¬ n + 1 < P N
223 220 221 222 3imtr3d φ n 0 n + 1 < P N ¬ P pCnt n + 1 < N ¬ n + 1 < P N
224 134 223 mt4d φ n 0 n + 1 < P N P pCnt n + 1 < N
225 224 adantr φ n 0 n + 1 < P N X P N 0 P pCnt n + 1 < N
226 dvdssubr P N X P N X P N X P N
227 12 35 226 syl2anc φ P N X P N X P N
228 6 227 mpbid φ P N X P N
229 228 ad2antrr φ n 0 n + 1 < P N X P N 0 P N X P N
230 207 nn0zd φ n 0 n + 1 < P N X P N 0 X P N
231 5 ad2antrr φ n 0 n + 1 < P N X P N 0 N 0
232 pcdvdsb P X P N N 0 N P pCnt X P N P N X P N
233 191 230 231 232 syl3anc φ n 0 n + 1 < P N X P N 0 N P pCnt X P N P N X P N
234 229 233 mpbird φ n 0 n + 1 < P N X P N 0 N P pCnt X P N
235 201 204 213 225 234 ltletrd φ n 0 n + 1 < P N X P N 0 P pCnt n + 1 < P pCnt X P N
236 191 194 198 235 pcadd2 φ n 0 n + 1 < P N X P N 0 P pCnt n + 1 = P pCnt n + 1 + X P N
237 190 236 pm2.61dane φ n 0 n + 1 < P N P pCnt n + 1 = P pCnt n + 1 + X P N
238 184 237 eqtr4d φ n 0 n + 1 < P N P pCnt X P N + n + 1 = P pCnt n + 1
239 199 nn0cnd φ n 0 n + 1 < P N P pCnt n + 1
240 238 239 eqeltrd φ n 0 n + 1 < P N P pCnt X P N + n + 1
241 240 238 subeq0bd φ n 0 n + 1 < P N P pCnt X P N + n + 1 P pCnt n + 1 = 0
242 181 241 eqtrd φ n 0 n + 1 < P N P pCnt X P N + n + 1 n + 1 = 0
243 242 oveq2d φ n 0 n + 1 < P N 0 + P pCnt X P N + n + 1 n + 1 = 0 + 0
244 00id 0 + 0 = 0
245 243 244 eqtr2di φ n 0 n + 1 < P N 0 = 0 + P pCnt X P N + n + 1 n + 1
246 178 245 eqeq12d φ n 0 n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = 0 P pCnt ( X - P N + n n) + P pCnt X P N + n + 1 n + 1 = 0 + P pCnt X P N + n + 1 n + 1
247 138 246 syl5ibr φ n 0 n + 1 < P N P pCnt ( X - P N + n n) = 0 P pCnt ( X P N + n + 1 n + 1 ) = 0
248 137 247 animpimp2impd n 0 φ n < P N P pCnt ( X - P N + n n) = 0 φ n + 1 < P N P pCnt ( X P N + n + 1 n + 1 ) = 0
249 94 100 106 112 125 248 nn0ind P N 1 0 φ P N 1 < P N P pCnt ( X P N + P N - 1 P N 1 ) = 0
250 88 249 mpcom φ P N 1 < P N P pCnt ( X P N + P N - 1 P N 1 ) = 0
251 86 250 mpd φ P pCnt ( X P N + P N - 1 P N 1 ) = 0
252 84 251 eqtr3d φ P pCnt ( X 1 P N 1 ) = 0
253 pcdiv P X X 0 P N P pCnt X P N = P pCnt X P pCnt P N
254 4 35 77 11 253 syl121anc φ P pCnt X P N = P pCnt X P pCnt P N
255 5 nn0zd φ N
256 pcid P N P pCnt P N = N
257 4 255 256 syl2anc φ P pCnt P N = N
258 257 oveq2d φ P pCnt X P pCnt P N = P pCnt X N
259 254 258 eqtrd φ P pCnt X P N = P pCnt X N
260 252 259 oveq12d φ P pCnt ( X 1 P N 1 ) + P pCnt X P N = 0 + P pCnt X - N
261 4 28 pccld φ P pCnt X 0
262 261 nn0zd φ P pCnt X
263 262 255 zsubcld φ P pCnt X N
264 263 zcnd φ P pCnt X N
265 264 addid2d φ 0 + P pCnt X - N = P pCnt X N
266 80 260 265 3eqtrd φ P pCnt ( X 1 P N 1 ) X P N = P pCnt X N
267 67 68 266 3eqtr3d φ P pCnt S = P pCnt X N
268 41 267 jca φ S P pCnt S = P pCnt X N