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

Theorem pgpfac1lem2 17643
 Description: Lemma for pgpfac1 17648. (Contributed by Mario Carneiro, 27-Apr-2016.)
Hypotheses
Ref Expression
pgpfac1.k mrClsSubGrp
pgpfac1.s
pgpfac1.b
pgpfac1.o
pgpfac1.e gEx
pgpfac1.z
pgpfac1.l
pgpfac1.p pGrp
pgpfac1.g
pgpfac1.n
pgpfac1.oe
pgpfac1.u SubGrp
pgpfac1.au
pgpfac1.w SubGrp
pgpfac1.i
pgpfac1.ss
pgpfac1.2 SubGrp
pgpfac1.c
pgpfac1.mg .g
Assertion
Ref Expression
pgpfac1lem2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem pgpfac1lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pgpfac1.c . . 3
21eldifbd 3455 . 2
31eldifad 3454 . . . . . . 7
43adantr 466 . . . . . 6
5 pgpfac1.u . . . . . . . . . 10 SubGrp
6 pgpfac1.p . . . . . . . . . . . 12 pGrp
7 pgpprm 17180 . . . . . . . . . . . 12 pGrp
86, 7syl 17 . . . . . . . . . . 11
9 prmz 14597 . . . . . . . . . . 11
108, 9syl 17 . . . . . . . . . 10
11 pgpfac1.mg . . . . . . . . . . 11 .g
1211subgmulgcl 16781 . . . . . . . . . 10 SubGrp
135, 10, 3, 12syl3anc 1264 . . . . . . . . 9
1413adantr 466 . . . . . . . 8
15 simpr 462 . . . . . . . 8
1614, 15eldifd 3453 . . . . . . 7
17 pgpfac1.k . . . . . . . 8 mrClsSubGrp
18 pgpfac1.s . . . . . . . 8
19 pgpfac1.b . . . . . . . 8
20 pgpfac1.o . . . . . . . 8
21 pgpfac1.e . . . . . . . 8 gEx
22 pgpfac1.z . . . . . . . 8
23 pgpfac1.l . . . . . . . 8
24 pgpfac1.g . . . . . . . 8
25 pgpfac1.n . . . . . . . 8
26 pgpfac1.oe . . . . . . . 8
27 pgpfac1.au . . . . . . . 8
28 pgpfac1.w . . . . . . . 8 SubGrp
29 pgpfac1.i . . . . . . . 8
30 pgpfac1.ss . . . . . . . 8
31 pgpfac1.2 . . . . . . . 8 SubGrp
3217, 18, 19, 20, 21, 22, 23, 6, 24, 25, 26, 5, 27, 28, 29, 30, 31pgpfac1lem1 17642 . . . . . . 7
3316, 32syldan 472 . . . . . 6
344, 33eleqtrrd 2520 . . . . 5
3534ex 435 . . . 4
36 eqid 2429 . . . . . 6
37 ablgrp 17370 . . . . . . . . . . . 12
3824, 37syl 17 . . . . . . . . . . 11
3919subgacs 16803 . . . . . . . . . . 11 SubGrp ACS
4038, 39syl 17 . . . . . . . . . 10 SubGrp ACS
4140acsmred 15513 . . . . . . . . 9 SubGrp Moore
4219subgss 16769 . . . . . . . . . . 11 SubGrp
435, 42syl 17 . . . . . . . . . 10
4443, 27sseldd 3471 . . . . . . . . 9
4517mrcsncl 15469 . . . . . . . . 9 SubGrp Moore SubGrp
4641, 44, 45syl2anc 665 . . . . . . . 8 SubGrp
4718, 46syl5eqel 2521 . . . . . . 7 SubGrp
4823lsmsubg2 17432 . . . . . . 7 SubGrp SubGrp SubGrp
4924, 47, 28, 48syl3anc 1264 . . . . . 6 SubGrp
5043, 13sseldd 3471 . . . . . . 7
5117mrcsncl 15469 . . . . . . 7 SubGrp Moore SubGrp
5241, 50, 51syl2anc 665 . . . . . 6 SubGrp
5336, 23, 49, 52lsmelvalm 17238 . . . . 5
54 eqid 2429 . . . . . . . . . 10
5519, 11, 54, 17cycsubg2 16805 . . . . . . . . 9
5638, 50, 55syl2anc 665 . . . . . . . 8
5756rexeqdv 3039 . . . . . . 7
58 ovex 6333 . . . . . . . . 9
5958rgenw 2793 . . . . . . . 8
60 oveq2 6313 . . . . . . . . . 10
6160eqeq2d 2443 . . . . . . . . 9
6254, 61rexrnmpt 6047 . . . . . . . 8
6359, 62mp1i 13 . . . . . . 7
6457, 63bitrd 256 . . . . . 6
6564rexbidv 2946 . . . . 5
66 rexcom 2997 . . . . . 6
6738ad2antrr 730 . . . . . . . . . . . 12
6830, 43sstrd 3480 . . . . . . . . . . . . . 14
6968adantr 466 . . . . . . . . . . . . 13
7069sselda 3470 . . . . . . . . . . . 12
71 simplr 760 . . . . . . . . . . . . 13
7250ad2antrr 730 . . . . . . . . . . . . 13
7319, 11mulgcl 16726 . . . . . . . . . . . . 13
7467, 71, 72, 73syl3anc 1264 . . . . . . . . . . . 12
7543, 3sseldd 3471 . . . . . . . . . . . . 13
7675ad2antrr 730 . . . . . . . . . . . 12
77 eqid 2429 . . . . . . . . . . . . 13
7819, 77, 36grpsubadd 16693 . . . . . . . . . . . 12
7967, 70, 74, 76, 78syl13anc 1266 . . . . . . . . . . 11
80 1zzd 10968 . . . . . . . . . . . . . 14
8110ad2antrr 730 . . . . . . . . . . . . . . 15
8271, 81zmulcld 11046 . . . . . . . . . . . . . 14
8319, 11, 77mulgdir 16734 . . . . . . . . . . . . . 14
8467, 80, 82, 76, 83syl13anc 1266 . . . . . . . . . . . . 13
8519, 11mulg1 16716 . . . . . . . . . . . . . . 15
8676, 85syl 17 . . . . . . . . . . . . . 14
8719, 11mulgass 16739 . . . . . . . . . . . . . . 15
8867, 71, 81, 76, 87syl13anc 1266 . . . . . . . . . . . . . 14
8986, 88oveq12d 6323 . . . . . . . . . . . . 13
9084, 89eqtrd 2470 . . . . . . . . . . . 12
9190eqeq1d 2431 . . . . . . . . . . 11
9279, 91bitr4d 259 . . . . . . . . . 10
93 eqcom 2438 . . . . . . . . . 10
94 eqcom 2438 . . . . . . . . . 10
9592, 93, 943bitr4g 291 . . . . . . . . 9
9695rexbidva 2943 . . . . . . . 8
97 risset 2960 . . . . . . . 8
9896, 97syl6bbr 266 . . . . . . 7
9998rexbidva 2943 . . . . . 6
10066, 99syl5bb 260 . . . . 5
10153, 65, 1003bitrd 282 . . . 4
10235, 101sylibd 217 . . 3
10338adantr 466 . . . . . 6
10475adantr 466 . . . . . 6
105 1z 10967 . . . . . . 7
106 id 23 . . . . . . . 8
107 zmulcl 10985 . . . . . . . 8
108106, 10, 107syl2anr 480 . . . . . . 7
109 zaddcl 10977 . . . . . . 7
110105, 108, 109sylancr 667 . . . . . 6
11119, 20odcl 17127 . . . . . . . . 9
112104, 111syl 17 . . . . . . . 8
113112nn0zd 11038 . . . . . . 7
114 hashcl 12535 . . . . . . . . . 10
11525, 114syl 17 . . . . . . . . 9
116115nn0zd 11038 . . . . . . . 8
117116adantr 466 . . . . . . 7
118 gcdcom 14458 . . . . . . . . 9
119110, 117, 118syl2anc 665 . . . . . . . 8
12019pgphash 17194 . . . . . . . . . . 11 pGrp
1216, 25, 120syl2anc 665 . . . . . . . . . 10
122121adantr 466 . . . . . . . . 9
123122oveq1d 6320 . . . . . . . 8
124 simpr 462 . . . . . . . . . . 11
12510adantr 466 . . . . . . . . . . 11
126 1zzd 10968 . . . . . . . . . . 11
127 gcdaddm 14467 . . . . . . . . . . 11
128124, 125, 126, 127syl3anc 1264 . . . . . . . . . 10
129 gcd1 14470 . . . . . . . . . . 11
130125, 129syl 17 . . . . . . . . . 10
131128, 130eqtr3d 2472 . . . . . . . . 9
13219grpbn0 16646 . . . . . . . . . . . . . 14
13338, 132syl 17 . . . . . . . . . . . . 13
134 hashnncl 12544 . . . . . . . . . . . . . 14
13525, 134syl 17 . . . . . . . . . . . . 13
136133, 135mpbird 235 . . . . . . . . . . . 12
1378, 136pccld 14763 . . . . . . . . . . 11
138137adantr 466 . . . . . . . . . 10
139 rpexp1i 14644 . . . . . . . . . 10
140125, 110, 138, 139syl3anc 1264 . . . . . . . . 9
141131, 140mpd 15 . . . . . . . 8
142119, 123, 1413eqtrd 2474 . . . . . . 7
14319, 20oddvds2 17155 . . . . . . . . 9
14438, 25, 75, 143syl3anc 1264 . . . . . . . 8
145144adantr 466 . . . . . . 7
146 rpdvds 14647 . . . . . . 7
147110, 113, 117, 142, 145, 146syl32anc 1272 . . . . . 6
14819, 20, 11odbezout 17147 . . . . . 6
149103, 104, 110, 147, 148syl31anc 1267 . . . . 5
15049ad2antrr 730 . . . . . . . 8 SubGrp
151 simpr 462 . . . . . . . 8
15211subgmulgcl 16781 . . . . . . . . 9 SubGrp
1531523expia 1207 . . . . . . . 8 SubGrp
154150, 151, 153syl2anc 665 . . . . . . 7
155 eleq1 2501 . . . . . . . 8
156155imbi2d 317 . . . . . . 7
157154, 156syl5ibcom 223 . . . . . 6
158157rexlimdva 2924 . . . . 5
159149, 158mpd 15 . . . 4
160159rexlimdva 2924 . . 3
161102, 160syld 45 . 2
1622, 161mt3d 128 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   wceq 1437   wcel 1870   wne 2625  wral 2782  wrex 2783  cvv 3087   cdif 3439   cin 3441   wss 3442   wpss 3443  c0 3767  csn 4002   class class class wbr 4426   cmpt 4484   crn 4855  cfv 5601  (class class class)co 6305  cfn 7577  c1 9539   caddc 9541   cmul 9543  cn 10609  cn0 10869  cz 10937  cexp 12269  chash 12512   cdvds 14283   cgcd 14442  cprime 14593   cpc 14749  cbs 15084   cplusg 15152  c0g 15297  Moorecmre 15439  mrClscmrc 15440  ACScacs 15442  cgrp 16620  csg 16622  .gcmg 16623  SubGrpcsubg 16762  cod 17116  gExcgex 17117   pGrp cpgp 17118  clsm 17221  cabl 17366 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-disj 4398  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-2o 7191  df-oadd 7194  df-omul 7195  df-er 7371  df-ec 7373  df-qs 7377  df-map 7482  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-sup 7962  df-inf 7963  df-oi 8025  df-card 8372  df-acn 8375  df-cda 8596  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-fz 11783  df-fzo 11914  df-fl 12025  df-mod 12094  df-seq 12211  df-exp 12270  df-fac 12457  df-bc 12485  df-hash 12513  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-dvds 14284  df-gcd 14443  df-prm 14594  df-pc 14750  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-0g 15299  df-mre 15443  df-mrc 15444  df-acs 15446  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-submnd 16534  df-grp 16624  df-minusg 16625  df-sbg 16626  df-mulg 16627  df-subg 16765  df-eqg 16767  df-ga 16895  df-cntz 16922  df-od 17120  df-pgp 17122  df-lsm 17223  df-cmn 17367  df-abl 17368 This theorem is referenced by:  pgpfac1lem4  17646
 Copyright terms: Public domain W3C validator