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

Theorem ablfac1eu 15308
 Description: The factorization of ablfac1b 15305 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to . (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
ablfac1.b
ablfac1.o
ablfac1.s
ablfac1.g
ablfac1.f
ablfac1.1
ablfac1c.d
ablfac1.2
ablfac1eu.1 DProd DProd
ablfac1eu.2
ablfac1eu.3
ablfac1eu.4
Assertion
Ref Expression
ablfac1eu
Distinct variable groups:   ,,,,   ,,,   ,,,,   ,   ,,,   ,,,   ,,   ,,,
Allowed substitution hints:   ()   (,,,)   ()   (,,)   (,)   ()   ()

Proof of Theorem ablfac1eu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ablfac1eu.1 . . . . 5 DProd DProd
21simpld 445 . . . 4 DProd
3 ablfac1eu.2 . . . 4
42, 3dprdf2 15242 . . 3 SubGrp
5 ffn 5389 . . 3 SubGrp
64, 5syl 15 . 2
7 ablfac1.b . . . . 5
8 ablfac1.o . . . . 5
9 ablfac1.s . . . . 5
10 ablfac1.g . . . . 5
11 ablfac1.f . . . . 5
12 ablfac1.1 . . . . 5
137, 8, 9, 10, 11, 12ablfac1b 15305 . . . 4 DProd
14 fvex 5539 . . . . . . . 8
157, 14eqeltri 2353 . . . . . . 7
1615rabex 4165 . . . . . 6
1716, 9dmmpti 5373 . . . . 5
1817a1i 10 . . . 4
1913, 18dprdf2 15242 . . 3 SubGrp
20 ffn 5389 . . 3 SubGrp
2119, 20syl 15 . 2
2211adantr 451 . . . 4
23 ffvelrn 5663 . . . . . 6 SubGrp SubGrp
2419, 23sylan 457 . . . . 5 SubGrp
257subgss 14622 . . . . 5 SubGrp
2624, 25syl 15 . . . 4
27 ssfi 7083 . . . 4
2822, 26, 27syl2anc 642 . . 3
29 ffvelrn 5663 . . . . . . 7 SubGrp SubGrp
304, 29sylan 457 . . . . . 6 SubGrp
317subgss 14622 . . . . . 6 SubGrp
3230, 31syl 15 . . . . 5
3330adantr 451 . . . . . . 7 SubGrp
34 ssfi 7083 . . . . . . . . 9
3522, 32, 34syl2anc 642 . . . . . . . 8
3635adantr 451 . . . . . . 7
37 simpr 447 . . . . . . 7
388odsubdvds 14882 . . . . . . 7 SubGrp
3933, 36, 37, 38syl3anc 1182 . . . . . 6
40 ablfac1eu.4 . . . . . . . 8
4112sselda 3180 . . . . . . . . . 10
42 prmz 12762 . . . . . . . . . 10
4341, 42syl 15 . . . . . . . . 9
44 ablfac1eu.3 . . . . . . . . 9
4544nn0zd 10115 . . . . . . . . . 10
46 ablgrp 15094 . . . . . . . . . . . . . . . 16
4710, 46syl 15 . . . . . . . . . . . . . . 15
487grpbn0 14511 . . . . . . . . . . . . . . 15
4947, 48syl 15 . . . . . . . . . . . . . 14
50 hashnncl 11354 . . . . . . . . . . . . . . 15
5111, 50syl 15 . . . . . . . . . . . . . 14
5249, 51mpbird 223 . . . . . . . . . . . . 13
5352adantr 451 . . . . . . . . . . . 12
5441, 53pccld 12903 . . . . . . . . . . 11
5554nn0zd 10115 . . . . . . . . . 10
567lagsubg 14679 . . . . . . . . . . . . 13 SubGrp
5730, 22, 56syl2anc 642 . . . . . . . . . . . 12
5840, 57eqbrtrrd 4045 . . . . . . . . . . 11
5953nnzd 10116 . . . . . . . . . . . 12
60 pcdvdsb 12921 . . . . . . . . . . . 12
6141, 59, 44, 60syl3anc 1182 . . . . . . . . . . 11
6258, 61mpbird 223 . . . . . . . . . 10
63 eluz2 10236 . . . . . . . . . 10
6445, 55, 62, 63syl3anbrc 1136 . . . . . . . . 9
65 dvdsexp 12584 . . . . . . . . 9
6643, 44, 64, 65syl3anc 1182 . . . . . . . 8
6740, 66eqbrtrd 4043 . . . . . . 7
6867adantr 451 . . . . . 6
6932sselda 3180 . . . . . . . . 9
707, 8odcl 14851 . . . . . . . . 9
7169, 70syl 15 . . . . . . . 8
7271nn0zd 10115 . . . . . . 7
73 hashcl 11350 . . . . . . . . . 10
7435, 73syl 15 . . . . . . . . 9
7574nn0zd 10115 . . . . . . . 8
7675adantr 451 . . . . . . 7
77 prmnn 12761 . . . . . . . . . . 11
7841, 77syl 15 . . . . . . . . . 10
7978, 54nnexpcld 11266 . . . . . . . . 9
8079nnzd 10116 . . . . . . . 8
8180adantr 451 . . . . . . 7
82 dvdstr 12562 . . . . . . 7
8372, 76, 81, 82syl3anc 1182 . . . . . 6
8439, 68, 83mp2and 660 . . . . 5
8532, 84ssrabdv 3252 . . . 4
86 id 19 . . . . . . . . 9
87 oveq1 5865 . . . . . . . . 9
8886, 87oveq12d 5876 . . . . . . . 8
8988breq2d 4035 . . . . . . 7
9089rabbidv 2780 . . . . . 6
9190, 9, 16fvmpt3i 5605 . . . . 5
9291adantl 452 . . . 4
9385, 92sseqtr4d 3215 . . 3
9479nnnn0d 10018 . . . . . 6
95 pcdvds 12916 . . . . . . . . . 10
9641, 53, 95syl2anc 642 . . . . . . . . 9
972adantr 451 . . . . . . . . . . . . . . 15 DProd
983adantr 451 . . . . . . . . . . . . . . 15
99 ablfac1.2 . . . . . . . . . . . . . . . 16
10099adantr 451 . . . . . . . . . . . . . . 15
10197, 98, 100dprdres 15263 . . . . . . . . . . . . . 14 DProd DProd DProd
102101simpld 445 . . . . . . . . . . . . 13 DProd
1034adantr 451 . . . . . . . . . . . . . . 15 SubGrp
104 fssres 5408 . . . . . . . . . . . . . . 15 SubGrp SubGrp
105103, 100, 104syl2anc 642 . . . . . . . . . . . . . 14 SubGrp
106 fdm 5393 . . . . . . . . . . . . . 14 SubGrp
107105, 106syl 15 . . . . . . . . . . . . 13
108 difss 3303 . . . . . . . . . . . . . 14
109108a1i 10 . . . . . . . . . . . . 13
110102, 107, 109dprdres 15263 . . . . . . . . . . . 12 DProd DProd DProd
111110simpld 445 . . . . . . . . . . 11 DProd
112 dprdsubg 15259 . . . . . . . . . . 11 DProd DProd SubGrp
113111, 112syl 15 . . . . . . . . . 10 DProd SubGrp
1147lagsubg 14679 . . . . . . . . . 10 DProd SubGrp DProd
115113, 22, 114syl2anc 642 . . . . . . . . 9 DProd
116 eqid 2283 . . . . . . . . . . . . . . 15
117116subg0cl 14629 . . . . . . . . . . . . . 14 DProd SubGrp DProd
118113, 117syl 15 . . . . . . . . . . . . 13 DProd
119 ne0i 3461 . . . . . . . . . . . . 13 DProd DProd
120118, 119syl 15 . . . . . . . . . . . 12 DProd
1217dprdssv 15251 . . . . . . . . . . . . . 14 DProd
122 ssfi 7083 . . . . . . . . . . . . . 14 DProd DProd
12322, 121, 122sylancl 643 . . . . . . . . . . . . 13 DProd
124 hashnncl 11354 . . . . . . . . . . . . 13 DProd DProd DProd
125123, 124syl 15 . . . . . . . . . . . 12 DProd DProd
126120, 125mpbird 223 . . . . . . . . . . 11 DProd
127126nnzd 10116 . . . . . . . . . 10 DProd
128 eqid 2283 . . . . . . . . . . . . . . . 16
12910adantr 451 . . . . . . . . . . . . . . . 16
13011adantr 451 . . . . . . . . . . . . . . . 16
131 ablfac1c.d . . . . . . . . . . . . . . . . . 18
132 ssrab2 3258 . . . . . . . . . . . . . . . . . 18
133131, 132eqsstri 3208 . . . . . . . . . . . . . . . . 17
134133a1i 10 . . . . . . . . . . . . . . . 16
135 ssid 3197 . . . . . . . . . . . . . . . . 17
136135a1i 10 . . . . . . . . . . . . . . . 16
1372, 3, 99dprdres 15263 . . . . . . . . . . . . . . . . . . 19 DProd DProd DProd
138137simpld 445 . . . . . . . . . . . . . . . . . 18 DProd
139 dprdsubg 15259 . . . . . . . . . . . . . . . . . . . . 21 DProd DProd SubGrp
140138, 139syl 15 . . . . . . . . . . . . . . . . . . . 20 DProd SubGrp
141 difss 3303 . . . . . . . . . . . . . . . . . . . . . . . 24
142141a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23
1432, 3, 142dprdres 15263 . . . . . . . . . . . . . . . . . . . . . 22 DProd DProd DProd
144143simpld 445 . . . . . . . . . . . . . . . . . . . . 21 DProd
145 dprdsubg 15259 . . . . . . . . . . . . . . . . . . . . 21 DProd DProd SubGrp
146144, 145syl 15 . . . . . . . . . . . . . . . . . . . 20 DProd SubGrp
147 fssres 5408 . . . . . . . . . . . . . . . . . . . . . . 23 SubGrp SubGrp
1484, 141, 147sylancl 643 . . . . . . . . . . . . . . . . . . . . . 22 SubGrp
149 fdm 5393 . . . . . . . . . . . . . . . . . . . . . 22 SubGrp
150148, 149syl 15 . . . . . . . . . . . . . . . . . . . . 21
151 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . 23
152151adantl 452 . . . . . . . . . . . . . . . . . . . . . 22
153 eldif 3162 . . . . . . . . . . . . . . . . . . . . . . 23
15435adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25
155116subg0cl 14629 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SubGrp
15630, 155syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
157156snssd 3760 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158157adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25
15940adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
16041adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
161 iddvdsexp 12552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
16243, 161sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
16358adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
16440, 75eqeltrrd 2358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
165 dvdstr 12562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
16643, 164, 59, 165syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
167166adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
168162, 163, 167mp2and 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
169 breq1 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
170169, 131elrab2 2925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
171160, 168, 170sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
172171ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
173172con3d 125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
174173impr 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
17544adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
176 elnn0 9967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177175, 176sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
178177ord 366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
179174, 178mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
180179oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
18178adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
182181nncnd 9762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
183182exp0d 11239 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
184159, 180, 1833eqtrd 2319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
185 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
186 hashsng 11356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187185, 186ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
188184, 187syl6reqr 2334 . . . . . . . . . . . . . . . . . . . . . . . . . 26
189 snfi 6941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
190 hashen 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
191189, 154, 190sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26
192188, 191mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . 25
193 fisseneq 7074 . . . . . . . . . . . . . . . . . . . . . . . . 25
194154, 158, 192, 193syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . 24
195116subg0cl 14629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 DProd SubGrp DProd
196140, 195syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 DProd
197196adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 DProd
198197snssd 3760 . . . . . . . . . . . . . . . . . . . . . . . 24 DProd
199194, 198eqsstr3d 3213 . . . . . . . . . . . . . . . . . . . . . . 23 DProd
200153, 199sylan2b 461 . . . . . . . . . . . . . . . . . . . . . 22 DProd
201152, 200eqsstrd 3212 . . . . . . . . . . . . . . . . . . . . 21 DProd
202144, 150, 140, 201dprdlub 15261 . . . . . . . . . . . . . . . . . . . 20 DProd DProd
203 eqid 2283 . . . . . . . . . . . . . . . . . . . . 21
204203lsmss2 14977 . . . . . . . . . . . . . . . . . . . 20 DProd SubGrp DProd SubGrp DProd DProd DProd DProd DProd
205140, 146, 202, 204syl3anc 1182 . . . . . . . . . . . . . . . . . . 19 DProd DProd DProd
206 disjdif 3526 . . . . . . . . . . . . . . . . . . . . . 22
207206a1i 10 . . . . . . . . . . . . . . . . . . . . 21
208 undif2 3530 . . . . . . . . . . . . . . . . . . . . . 22
209 ssequn1 3345 . . . . . . . . . . . . . . . . . . . . . . 23
21099, 209sylib 188 . . . . . . . . . . . . . . . . . . . . . 22
211208, 210syl5req 2328 . . . . . . . . . . . . . . . . . . . . 21
2124, 207, 211, 203, 2dprdsplit 15283 . . . . . . . . . . . . . . . . . . . 20 DProd DProd DProd
2131simprd 449 . . . . . . . . . . . . . . . . . . . 20 DProd
214212, 213eqtr3d 2317 . . . . . . . . . . . . . . . . . . 19 DProd DProd
215205, 214eqtr3d 2317 . . . . . . . . . . . . . . . . . 18 DProd
216138, 215jca 518 . . . . . . . . . . . . . . . . 17 DProd DProd
217216adantr 451 . . . . . . . . . . . . . . . 16 DProd DProd
2184, 99, 104syl2anc 642 . . . . . . . . . . . . . . . . . 18 SubGrp
219218, 106syl 15 . . . . . . . . . . . . . . . . 17
220219adantr 451 . . . . . . . . . . . . . . . 16
22199sselda 3180 . . . . . . . . . . . . . . . . . 18
222221, 44syldan 456 . . . . . . . . . . . . . . . . 17
223222adantlr 695 . . . . . . . . . . . . . . . 16
224 fvres 5542 . . . . . . . . . . . . . . . . . . . 20
225224adantl 452 . . . . . . . . . . . . . . . . . . 19
226225fveq2d 5529 . . . . . . . . . . . . . . . . . 18
227221, 40syldan 456 . . . . . . . . . . . . . . . . . 18
228226, 227eqtrd 2315 . . . . . . . . . . . . . . . . 17
229228adantlr 695 . . . . . . . . . . . . . . . 16
230 simpr 447 . . . . . . . . . . . . . . . 16
231 fzfid 11035 . . . . . . . . . . . . . . . . . 18
232 prmnn 12761 . . . . . . . . . . . . . . . . . . . . . 22
2332323ad2ant2 977 . . . . . . . . . . . . . . . . . . . . 21
234 prmz 12762 . . . . . . . . . . . . . . . . . . . . . . 23
235 dvdsle 12574 . . . . . . . . . . . . . . . . . . . . . . 23
236234, 52, 235syl2anr 464 . . . . . . . . . . . . . . . . . . . . . 22
2372363impia 1148 . . . . . . . . . . . . . . . . . . . . 21
23852nnzd 10116 . . . . . . . . . . . . . . . . . . . . . . 23
2392383ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . 22
240 fznn 10852 . . . . . . . . . . . . . . . . . . . . . 22
241239, 240syl 15 . . . . . . . . . . . . . . . . . . . . 21
242233, 237, 241mpbir2and 888 . . . . . . . . . . . . . . . . . . . 20
243242rabssdv 3253 . . . . . . . . . . . . . . . . . . 19
244131, 243syl5eqss 3222 . . . . . . . . . . . . . . . . . 18
245 ssfi 7083 . . . . . . . . . . . . . . . . . 18
246231, 244, 245syl2anc 642 . . . . . . . . . . . . . . . . 17
247246adantr 451 . . . . . . . . . . . . . . . 16
2487, 8, 128, 129, 130, 134, 131, 136, 217, 220, 223, 229, 230, 247ablfac1eulem 15307 . . . . . . . . . . . . . . 15 DProd
249248ralrimiva 2626 . . . . . . . . . . . . . 14 DProd
250249adantr 451 . . . . . . . . . . . . 13 DProd
251 id 19 . . . . . . . . . . . . . . . 16
252 sneq 3651 . . . . . . . . . . . . . . . . . . . 20
253252difeq2d 3294 . . . . . . . . . . . . . . . . . . 19
254253reseq2d 4955 . . . . . . . . . . . . . . . . . 18
255254oveq2d 5874 . . . . . . . . . . . . . . . . 17 DProd DProd
256255fveq2d 5529 . . . . . . . . . . . . . . . 16 DProd DProd
257251, 256breq12d 4036 . . . . . . . . . . . . . . 15 DProd DProd
258257notbid 285 . . . . . . . . . . . . . 14 DProd DProd
259258rspcv 2880 . . . . . . . . . . . . 13 DProd DProd
26041, 250, 259sylc 56 . . . . . . . . . . . 12 DProd
261 coprm 12779 . . . . . . . . . . . . 13 DProd DProd DProd
26241, 127, 261syl2anc 642 . . . . . . . . . . . 12 DProd DProd
263260, 262mpbid 201 . . . . . . . . . . 11 DProd
264 rpexp1i 12800 . . . . . . . . . . . 12 DProd DProd DProd
26543, 127, 54, 264syl3anc 1182 . . . . . . . . . . 11 DProd DProd
266263, 265mpd 14 . . . . . . . . . 10 DProd
267 coprmdvds2 12782 . . . . . . . . . 10 DProd DProd DProd DProd
26880, 127, 59, 266, 267syl31anc 1185 . . . . . . . . 9 DProd DProd
26996, 115, 268mp2and 660 . . . . . . . 8 DProd
270 eqid 2283 . . . . . . . . . 10 Cntz Cntz
271 inss1 3389 . . . . . . . . . . . . . 14
272271a1i 10 . . . . . . . . . . . . 13
273102, 107, 272dprdres 15263 . . . . . . . . . . . 12 DProd DProd DProd
274273simpld 445 . . . . . . . . . . 11 DProd
275 dprdsubg 15259 . . . . . . . . . . 11 DProd DProd SubGrp
276274, 275syl 15 . . . . . . . . . 10 DProd SubGrp
277 inass 3379 . . . . . . . . . . . . 13
278 disjdif 3526 . . . . . . . . . . . . . 14
279278ineq2i 3367 . . . . . . . . . . . . 13
280 in0 3480 . . . . . . . . . . . . 13
281277, 279, 2803eqtri 2307 . . . . . . . . . . . 12
282281a1i 10 . . . . . . . . . . 11
283102, 107, 272, 109, 282, 116dprddisj2 15274 . . . . . . . . . 10 DProd DProd
284102, 107, 272, 109, 282, 270dprdcntz2 15273 . . . . . . . . . 10 DProd Cntz DProd
2857dprdssv 15251 . . . . . . . . . . 11 DProd
286 ssfi 7083 . . . . . . . . . . 11 DProd DProd
28722, 285, 286sylancl 643 . . . . . . . . . 10 DProd
288203, 116, 270, 276, 113, 283, 284, 287, 123lsmhash 15014 . . . . . . . . 9 DProd DProd DProd DProd
289 inundif 3532 . . . . . . . . . . . . . 14
290289eqcomi 2287 . . . . . . . . . . . . 13
291290a1i 10 . . . . . . . . . . . 12
292105, 282, 291, 203, 102dprdsplit 15283 . . . . . . . . . . 11 DProd DProd DProd
293215adantr 451 . . . . . . . . . . 11 DProd
294292, 293eqtr3d 2317 . . . . . . . . . 10 DProd DProd
295294fveq2d 5529 . . . . . . . . 9 DProd DProd
296 snssi 3759 . . . . . . . . . . . . . . . . 17
297296adantl 452 . . . . . . . . . . . . . . . 16
298 dfss1 3373 . . . . . . . . . . . . . . . 16
299297, 298sylib 188 . . . . . . . . . . . . . . 15
300299reseq2d 4955 . . . . . . . . . . . . . 14
301300oveq2d 5874 . . . . . . . . . . . . 13 DProd DProd
302102adantr 451 . . . . . . . . . . . . . 14 DProd
303219ad2antrr 706 . . . . . . . . . . . . . 14
304 simpr 447 . . . . . . . . . . . . . 14
305302, 303, 304dpjlem 15286 . . . . . . . . . . . . 13 DProd
306224adantl 452 . . . . . . . . . . . . 13
307301, 305, 3063eqtrd 2319 . . . . . . . . . . . 12 DProd
308 simprr 733 . . . . . . . . . . . . . . . . . 18
309 disjsn 3693 . . . . . . . . . . . . . . . . . 18
310308, 309sylibr 203 . . . . . . . . . . . . . . . . 17
311310reseq2d 4955 . . . . . . . . . . . . . . . 16
312 res0 4959 . . . . . . . . . . . . . . . 16
313311, 312syl6eq 2331 . . . . . . . . . . . . . . 15
314313oveq2d 5874 . . . . . . . . . . . . . 14 DProd DProd
315116dprd0 15266 . . . . . . . . . . . . . . . . 17 DProd DProd
31647, 315syl 15 . . . . . . . . . . . . . . . 16 DProd DProd
317316simprd 449 . . . . . . . . . . . . . . 15 DProd
318317adantr 451 . . . . . . . . . . . . . 14 DProd
319314, 318, 1943eqtrd 2319 . . . . . . . . . . . . 13 DProd
320319anassrs 629 . . . . . . . . . . . 12 DProd
321307, 320pm2.61dan 766 . . . . . . . . . . 11 DProd
322321fveq2d 5529 . . . . . . . . . 10 DProd
323322oveq1d 5873 . . . . . . . . 9 DProd DProd DProd
324288, 295, 3233eqtr3d 2323 . . . . . . . 8 DProd
325269, 324breqtrd 4047 . . . . . . 7 DProd DProd
326126nnne0d 9790 . . . . . . . 8 DProd
327 dvdsmulcr 12558 . . . . . . . 8 DProd DProd DProd DProd
32880, 75, 127, 326, 327syl112anc 1186 . . . . . . 7 DProd DProd
329325, 328mpbid 201 . . . . . 6
330 dvdseq 12576 . . . . . 6
33174, 94, 67, 329, 330syl22anc 1183 . . . . 5
3327, 8, 9, 10, 11, 12ablfac1a 15304 . . . . 5
333331, 332eqtr4d 2318 . . . 4
334 hashen 11346 . . . . 5
33535, 28, 334syl2anc 642 . . . 4
336333, 335mpbid 201 . . 3
337 fisseneq 7074 . . 3
33828, 93, 336, 337syl3anc 1182 . 2
3396, 21, 338eqfnfvd 5625 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934   wceq 1623   wcel 1684   wne 2446  wral 2543  crab 2547  cvv 2788   cdif 3149   cun 3150   cin 3151   wss 3152  c0 3455  csn 3640   class class class wbr 4023   cmpt 4077   cdm 4689   cres 4691   wfn 5250  wf 5251  cfv 5255  (class class class)co 5858   cen 6860  cfn 6863  cc0 8737  c1 8738   cmul 8742   cle 8868  cn 9746  cn0 9965  cz 10024  cuz 10230  cfz 10782  cexp 11104  chash 11337   cdivides 12531   cgcd 12685  cprime 12758   cpc 12889  cbs 13148  c0g 13400  cgrp 14362  SubGrpcsubg 14615  Cntzccntz 14791  cod 14840  clsm 14945  cabel 15090   DProd cdprd 15231 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-iin 3908  df-disj 3994  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078  df-1st 6122  df-2nd 6123  df-tpos 6234  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-omul 6484  df-er 6660  df-ec 6662  df-qs 6666  df-map 6774  df-ixp 6818  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-acn 7575  df-cda 7794  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-q 10317  df-rp 10355  df-fz 10783  df-fzo 10871  df-fl 10925  df-mod 10974  df-seq 11047  df-exp 11105  df-fac 11289  df-bc 11316  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-clim 11962  df-sum 12159  df-dvds 12532  df-gcd 12686  df-prm 12759  df-pc 12890  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-0g 13404  df-gsum 13405  df-mre 13488  df-mrc 13489  df-acs 13491  df-mnd 14367  df-mhm 14415  df-submnd 14416  df-grp 14489  df-minusg 14490  df-sbg 14491  df-mulg 14492  df-subg 14618  df-eqg 14620  df-ghm 14681  df-gim 14723  df-ga 14744  df-cntz 14793  df-oppg 14819  df-od 14844  df-lsm 14947  df-pj1 14948  df-cmn 15091  df-abl 15092  df-dprd 15233
 Copyright terms: Public domain W3C validator