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={\mathrm{Base}}_G$$
	gexod.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
	gexod.3	$$⊢O=\mathrm{od}\left(G\right)$$
Assertion	gexod	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(A\right)\parallel E$$

Proof

Step	Hyp	Ref	Expression
1		gexod.1	$$⊢X={\mathrm{Base}}_G$$
2		gexod.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
3		gexod.3	$$⊢O=\mathrm{od}\left(G\right)$$
4		eqid	$$⊢{\cdot }_G={\cdot }_G$$
5		eqid	$$⊢0_G=0_G$$
6	1 2 4 5	gexid	$$⊢A\in X\to E{\cdot }_{G}A=0_G$$
7	6	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to E{\cdot }_{G}A=0_G$$
8	1 2	gexcl	$$⊢G\in \mathrm{Grp}\to E\in {\mathbb{N}}_0$$
9	8	adantr	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to E\in {\mathbb{N}}_0$$
10	9	nn0zd	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to E\in \mathbb{Z}$$
11	1 3 4 5	oddvds	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge E\in \mathbb{Z}\right)\to \left(O\left(A\right)\parallel E\leftrightarrow E{\cdot }_{G}A=0_G\right)$$
12	10 11	mpd3an3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(O\left(A\right)\parallel E\leftrightarrow E{\cdot }_{G}A=0_G\right)$$
13	7 12	mpbird	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(A\right)\parallel E$$