Theorem gexod

Description: Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexod.1	|- X = ( Base ` G )
	gexod.2	|- E = ( gEx ` G )
	gexod.3	|- O = ( od ` G )
Assertion	gexod	|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) || E )

Proof

Step	Hyp	Ref	Expression
1		gexod.1	|- X = ( Base ` G )
2		gexod.2	|- E = ( gEx ` G )
3		gexod.3	|- O = ( od ` G )
4		eqid	|- ( .g ` G ) = ( .g ` G )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	1 2 4 5	gexid	|- ( A e. X -> ( E ( .g ` G ) A ) = ( 0g ` G ) )
7	6	adantl	|- ( ( G e. Grp /\ A e. X ) -> ( E ( .g ` G ) A ) = ( 0g ` G ) )
8	1 2	gexcl	|- ( G e. Grp -> E e. NN0 )
9	8	adantr	|- ( ( G e. Grp /\ A e. X ) -> E e. NN0 )
10	9	nn0zd	|- ( ( G e. Grp /\ A e. X ) -> E e. ZZ )
11	1 3 4 5	oddvds	|- ( ( G e. Grp /\ A e. X /\ E e. ZZ ) -> ( ( O ` A ) || E <-> ( E ( .g ` G ) A ) = ( 0g ` G ) ) )
12	10 11	mpd3an3	|- ( ( G e. Grp /\ A e. X ) -> ( ( O ` A ) || E <-> ( E ( .g ` G ) A ) = ( 0g ` G ) ) )
13	7 12	mpbird	|- ( ( G e. Grp /\ A e. X ) -> ( O ` A ) || E )