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 ) )