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