Metamath Proof Explorer

Theorem gexcl2

Description: The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl2.1 
|- X = ( Base ` G )
gexcl2.2 
|- E = ( gEx ` G )
Assertion gexcl2 
|- ( ( G e. Grp /\ X e. Fin ) -> E e. NN )

Proof

Step Hyp Ref Expression
1 gexcl2.1 
 |-  X = ( Base ` G )
2 gexcl2.2 
 |-  E = ( gEx ` G )
3 eqid 
 |-  ( od ` G ) = ( od ` G )
4 1 3 odcl2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) e. NN )
5 1 3 oddvds2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) || ( # ` X ) )
6 4 nnzd 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) e. ZZ )
7 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
8 7 3ad2ant1 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> X =/= (/) )
9 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
10 9 3ad2ant2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
11 8 10 mpbird 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( # ` X ) e. NN )
12 dvdsle 
 |-  ( ( ( ( od ` G ) ` x ) e. ZZ /\ ( # ` X ) e. NN ) -> ( ( ( od ` G ) ` x ) || ( # ` X ) -> ( ( od ` G ) ` x ) <_ ( # ` X ) ) )
13 6 11 12 syl2anc 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( ( od ` G ) ` x ) || ( # ` X ) -> ( ( od ` G ) ` x ) <_ ( # ` X ) ) )
14 5 13 mpd 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) <_ ( # ` X ) )
15 11 nnzd 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( # ` X ) e. ZZ )
16 fznn 
 |-  ( ( # ` X ) e. ZZ -> ( ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) <-> ( ( ( od ` G ) ` x ) e. NN /\ ( ( od ` G ) ` x ) <_ ( # ` X ) ) ) )
17 15 16 syl 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) <-> ( ( ( od ` G ) ` x ) e. NN /\ ( ( od ` G ) ` x ) <_ ( # ` X ) ) ) )
18 4 14 17 mpbir2and 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) )
19 18 3expa 
 |-  ( ( ( G e. Grp /\ X e. Fin ) /\ x e. X ) -> ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) )
20 19 ralrimiva 
 |-  ( ( G e. Grp /\ X e. Fin ) -> A. x e. X ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) )
21 1 2 3 gexcl3 
 |-  ( ( G e. Grp /\ A. x e. X ( ( od ` G ) ` x ) e. ( 1 ... ( # ` X ) ) ) -> E e. NN )
22 20 21 syldan 
 |-  ( ( G e. Grp /\ X e. Fin ) -> E e. NN )