Theorem oddvdsi

Description: Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
	odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	oddvdsi	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge O\left(A\right)\parallel N\right)\to N\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		simp3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge O\left(A\right)\parallel N\right)\to O\left(A\right)\parallel N$$
6		dvdszrcl	$$⊢O\left(A\right)\parallel N\to \left(O\left(A\right)\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
7	6	simprd	$$⊢O\left(A\right)\parallel N\to N\in \mathbb{Z}$$
8	1 2 3 4	oddvds	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge N\in \mathbb{Z}\right)\to \left(O\left(A\right)\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
9	7 8	syl3an3	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge O\left(A\right)\parallel N\right)\to \left(O\left(A\right)\parallel N\leftrightarrow N\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
10	5 9	mpbid	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\wedge O\left(A\right)\parallel N\right)\to N\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$