Metamath Proof Explorer


Theorem pgpfi

Description: The converse to pgpfi1 . A finite group is a P -group iff it has size some power of P . (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis pgpfi.1 X = Base G
Assertion pgpfi G Grp X Fin P pGrp G P n 0 X = P n

Proof

Step Hyp Ref Expression
1 pgpfi.1 X = Base G
2 eqid od G = od G
3 1 2 ispgp P pGrp G P G Grp x X m 0 od G x = P m
4 simprl G Grp X Fin P x X m 0 od G x = P m P
5 1 grpbn0 G Grp X
6 5 ad2antrr G Grp X Fin P x X m 0 od G x = P m X
7 hashnncl X Fin X X
8 7 ad2antlr G Grp X Fin P x X m 0 od G x = P m X X
9 6 8 mpbird G Grp X Fin P x X m 0 od G x = P m X
10 4 9 pccld G Grp X Fin P x X m 0 od G x = P m P pCnt X 0
11 10 nn0red G Grp X Fin P x X m 0 od G x = P m P pCnt X
12 11 leidd G Grp X Fin P x X m 0 od G x = P m P pCnt X P pCnt X
13 10 nn0zd G Grp X Fin P x X m 0 od G x = P m P pCnt X
14 pcid P P pCnt X P pCnt P P pCnt X = P pCnt X
15 4 13 14 syl2anc G Grp X Fin P x X m 0 od G x = P m P pCnt P P pCnt X = P pCnt X
16 12 15 breqtrrd G Grp X Fin P x X m 0 od G x = P m P pCnt X P pCnt P P pCnt X
17 16 ad2antrr G Grp X Fin P x X m 0 od G x = P m p p = P P pCnt X P pCnt P P pCnt X
18 simpr G Grp X Fin P x X m 0 od G x = P m p p = P p = P
19 18 oveq1d G Grp X Fin P x X m 0 od G x = P m p p = P p pCnt X = P pCnt X
20 18 oveq1d G Grp X Fin P x X m 0 od G x = P m p p = P p pCnt P P pCnt X = P pCnt P P pCnt X
21 17 19 20 3brtr4d G Grp X Fin P x X m 0 od G x = P m p p = P p pCnt X p pCnt P P pCnt X
22 simp-4l G Grp X Fin P x X m 0 od G x = P m p p X G Grp
23 simplr G Grp X Fin P x X m 0 od G x = P m X Fin
24 23 ad2antrr G Grp X Fin P x X m 0 od G x = P m p p X X Fin
25 simplr G Grp X Fin P x X m 0 od G x = P m p p X p
26 simpr G Grp X Fin P x X m 0 od G x = P m p p X p X
27 1 2 odcau G Grp X Fin p p X g X od G g = p
28 22 24 25 26 27 syl31anc G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p
29 25 adantr G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p
30 prmz p p
31 iddvds p p p
32 29 30 31 3syl G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p p
33 simprr G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p od G g = p
34 32 33 breqtrrd G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p od G g
35 simplrr G Grp X Fin P x X m 0 od G x = P m p x X m 0 od G x = P m
36 fveqeq2 x = g od G x = P m od G g = P m
37 36 rexbidv x = g m 0 od G x = P m m 0 od G g = P m
38 37 rspccva x X m 0 od G x = P m g X m 0 od G g = P m
39 35 38 sylan G Grp X Fin P x X m 0 od G x = P m p g X m 0 od G g = P m
40 39 ad2ant2r G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p m 0 od G g = P m
41 4 ad3antrrr G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p P
42 prmnn p p
43 29 42 syl G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p
44 33 43 eqeltrd G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p od G g
45 pcprmpw P od G g m 0 od G g = P m od G g = P P pCnt od G g
46 41 44 45 syl2anc G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p m 0 od G g = P m od G g = P P pCnt od G g
47 40 46 mpbid G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p od G g = P P pCnt od G g
48 34 47 breqtrd G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p P P pCnt od G g
49 41 44 pccld G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p P pCnt od G g 0
50 prmdvdsexpr p P P pCnt od G g 0 p P P pCnt od G g p = P
51 29 41 49 50 syl3anc G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p P P pCnt od G g p = P
52 48 51 mpd G Grp X Fin P x X m 0 od G x = P m p p X g X od G g = p p = P
53 28 52 rexlimddv G Grp X Fin P x X m 0 od G x = P m p p X p = P
54 53 ex G Grp X Fin P x X m 0 od G x = P m p p X p = P
55 54 necon3ad G Grp X Fin P x X m 0 od G x = P m p p P ¬ p X
56 55 imp G Grp X Fin P x X m 0 od G x = P m p p P ¬ p X
57 simplr G Grp X Fin P x X m 0 od G x = P m p p P p
58 9 ad2antrr G Grp X Fin P x X m 0 od G x = P m p p P X
59 pceq0 p X p pCnt X = 0 ¬ p X
60 57 58 59 syl2anc G Grp X Fin P x X m 0 od G x = P m p p P p pCnt X = 0 ¬ p X
61 56 60 mpbird G Grp X Fin P x X m 0 od G x = P m p p P p pCnt X = 0
62 prmnn P P
63 62 ad2antrl G Grp X Fin P x X m 0 od G x = P m P
64 63 10 nnexpcld G Grp X Fin P x X m 0 od G x = P m P P pCnt X
65 64 ad2antrr G Grp X Fin P x X m 0 od G x = P m p p P P P pCnt X
66 57 65 pccld G Grp X Fin P x X m 0 od G x = P m p p P p pCnt P P pCnt X 0
67 66 nn0ge0d G Grp X Fin P x X m 0 od G x = P m p p P 0 p pCnt P P pCnt X
68 61 67 eqbrtrd G Grp X Fin P x X m 0 od G x = P m p p P p pCnt X p pCnt P P pCnt X
69 21 68 pm2.61dane G Grp X Fin P x X m 0 od G x = P m p p pCnt X p pCnt P P pCnt X
70 69 ralrimiva G Grp X Fin P x X m 0 od G x = P m p p pCnt X p pCnt P P pCnt X
71 hashcl X Fin X 0
72 71 ad2antlr G Grp X Fin P x X m 0 od G x = P m X 0
73 72 nn0zd G Grp X Fin P x X m 0 od G x = P m X
74 64 nnzd G Grp X Fin P x X m 0 od G x = P m P P pCnt X
75 pc2dvds X P P pCnt X X P P pCnt X p p pCnt X p pCnt P P pCnt X
76 73 74 75 syl2anc G Grp X Fin P x X m 0 od G x = P m X P P pCnt X p p pCnt X p pCnt P P pCnt X
77 70 76 mpbird G Grp X Fin P x X m 0 od G x = P m X P P pCnt X
78 oveq2 n = P pCnt X P n = P P pCnt X
79 78 breq2d n = P pCnt X X P n X P P pCnt X
80 79 rspcev P pCnt X 0 X P P pCnt X n 0 X P n
81 10 77 80 syl2anc G Grp X Fin P x X m 0 od G x = P m n 0 X P n
82 pcprmpw2 P X n 0 X P n X = P P pCnt X
83 pcprmpw P X n 0 X = P n X = P P pCnt X
84 82 83 bitr4d P X n 0 X P n n 0 X = P n
85 4 9 84 syl2anc G Grp X Fin P x X m 0 od G x = P m n 0 X P n n 0 X = P n
86 81 85 mpbid G Grp X Fin P x X m 0 od G x = P m n 0 X = P n
87 4 86 jca G Grp X Fin P x X m 0 od G x = P m P n 0 X = P n
88 87 3adantr2 G Grp X Fin P G Grp x X m 0 od G x = P m P n 0 X = P n
89 88 ex G Grp X Fin P G Grp x X m 0 od G x = P m P n 0 X = P n
90 3 89 syl5bi G Grp X Fin P pGrp G P n 0 X = P n
91 1 pgpfi1 G Grp P n 0 X = P n P pGrp G
92 91 3expia G Grp P n 0 X = P n P pGrp G
93 92 rexlimdv G Grp P n 0 X = P n P pGrp G
94 93 expimpd G Grp P n 0 X = P n P pGrp G
95 94 adantr G Grp X Fin P n 0 X = P n P pGrp G
96 90 95 impbid G Grp X Fin P pGrp G P n 0 X = P n