Metamath Proof Explorer

Theorem pgpfi1

Description: A finite group with order a power of a prime P is a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis pgpfi1.1 
|- X = ( Base ` G )
Assertion pgpfi1 
|- ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) -> ( ( # ` X ) = ( P ^ N ) -> P pGrp G ) )

Proof

Step Hyp Ref Expression
1 pgpfi1.1 
 |-  X = ( Base ` G )
2 simpl2 
 |-  ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) -> P e. Prime )
3 simpl1 
 |-  ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) -> G e. Grp )
4 simpll3 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> N e. NN0 )
5 3 adantr 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> G e. Grp )
6 simplr 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( # ` X ) = ( P ^ N ) )
7 2 adantr 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> P e. Prime )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 7 8 syl 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> P e. NN )
10 9 4 nnexpcld 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( P ^ N ) e. NN )
11 10 nnnn0d 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( P ^ N ) e. NN0 )
12 6 11 eqeltrd 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( # ` X ) e. NN0 )
13 1 fvexi 
 |-  X e. _V
14 hashclb 
 |-  ( X e. _V -> ( X e. Fin <-> ( # ` X ) e. NN0 ) )
15 13 14 ax-mp 
 |-  ( X e. Fin <-> ( # ` X ) e. NN0 )
16 12 15 sylibr 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> X e. Fin )
17 simpr 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> x e. X )
18 eqid 
 |-  ( od ` G ) = ( od ` G )
19 1 18 oddvds2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) || ( # ` X ) )
20 5 16 17 19 syl3anc 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( ( od ` G ) ` x ) || ( # ` X ) )
21 20 6 breqtrd 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( ( od ` G ) ` x ) || ( P ^ N ) )
22 oveq2 
 |-  ( n = N -> ( P ^ n ) = ( P ^ N ) )
23 22 breq2d 
 |-  ( n = N -> ( ( ( od ` G ) ` x ) || ( P ^ n ) <-> ( ( od ` G ) ` x ) || ( P ^ N ) ) )
24 23 rspcev 
 |-  ( ( N e. NN0 /\ ( ( od ` G ) ` x ) || ( P ^ N ) ) -> E. n e. NN0 ( ( od ` G ) ` x ) || ( P ^ n ) )
25 4 21 24 syl2anc 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> E. n e. NN0 ( ( od ` G ) ` x ) || ( P ^ n ) )
26 1 18 odcl2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) e. NN )
27 5 16 17 26 syl3anc 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( ( od ` G ) ` x ) e. NN )
28 pcprmpw2 
 |-  ( ( P e. Prime /\ ( ( od ` G ) ` x ) e. NN ) -> ( E. n e. NN0 ( ( od ` G ) ` x ) || ( P ^ n ) <-> ( ( od ` G ) ` x ) = ( P ^ ( P pCnt ( ( od ` G ) ` x ) ) ) ) )
29 pcprmpw 
 |-  ( ( P e. Prime /\ ( ( od ` G ) ` x ) e. NN ) -> ( E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) <-> ( ( od ` G ) ` x ) = ( P ^ ( P pCnt ( ( od ` G ) ` x ) ) ) ) )
30 28 29 bitr4d 
 |-  ( ( P e. Prime /\ ( ( od ` G ) ` x ) e. NN ) -> ( E. n e. NN0 ( ( od ` G ) ` x ) || ( P ^ n ) <-> E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) )
31 7 27 30 syl2anc 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> ( E. n e. NN0 ( ( od ` G ) ` x ) || ( P ^ n ) <-> E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) )
32 25 31 mpbid 
 |-  ( ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) /\ x e. X ) -> E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) )
33 32 ralrimiva 
 |-  ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) -> A. x e. X E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) )
34 1 18 ispgp 
 |-  ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. X E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) )
35 2 3 33 34 syl3anbrc 
 |-  ( ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) /\ ( # ` X ) = ( P ^ N ) ) -> P pGrp G )
36 35 ex 
 |-  ( ( G e. Grp /\ P e. Prime /\ N e. NN0 ) -> ( ( # ` X ) = ( P ^ N ) -> P pGrp G ) )