This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gexdvds3

Description: The exponent of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 24-Apr-2016)

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

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 oddvds2 
 |-  ( ( G e. Grp /\ X e. Fin /\ x e. X ) -> ( ( od ` G ) ` x ) || ( # ` X ) )
5 4 3expa 
 |-  ( ( ( G e. Grp /\ X e. Fin ) /\ x e. X ) -> ( ( od ` G ) ` x ) || ( # ` X ) )
6 5 ralrimiva 
 |-  ( ( G e. Grp /\ X e. Fin ) -> A. x e. X ( ( od ` G ) ` x ) || ( # ` X ) )
7 hashcl 
 |-  ( X e. Fin -> ( # ` X ) e. NN0 )
8 7 adantl 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( # ` X ) e. NN0 )
9 8 nn0zd 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( # ` X ) e. ZZ )
10 1 2 3 gexdvds2 
 |-  ( ( G e. Grp /\ ( # ` X ) e. ZZ ) -> ( E || ( # ` X ) <-> A. x e. X ( ( od ` G ) ` x ) || ( # ` X ) ) )
11 9 10 syldan 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( E || ( # ` X ) <-> A. x e. X ( ( od ` G ) ` x ) || ( # ` X ) ) )
12 6 11 mpbird 
 |-  ( ( G e. Grp /\ X e. Fin ) -> E || ( # ` X ) )