Theorem odcl

Description: The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	$$⊢X={\mathrm{Base}}_G$$
	odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
Assertion	odcl	$$⊢A\in X\to O\left(A\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		eqid	$$⊢{\cdot }_G={\cdot }_G$$
4		eqid	$$⊢0_G=0_G$$
5		eqid	$$⊢\left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}=\left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}$$
6	1 3 4 2 5	odlem1	$$⊢A\in X\to \left(\left(O\left(A\right)=0\wedge \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}=\varnothing \right)\vee O\left(A\right)\in \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}\right)$$
7		simpl	$$⊢\left(O\left(A\right)=0\wedge \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}=\varnothing \right)\to O\left(A\right)=0$$
8		elrabi	$$⊢O\left(A\right)\in \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}\to O\left(A\right)\in \mathbb{N}$$
9	7 8	orim12i	$$⊢\left(\left(O\left(A\right)=0\wedge \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}=\varnothing \right)\vee O\left(A\right)\in \left\{y\in \mathbb{N}|y{\cdot }_{G}A=0_G\right\}\right)\to \left(O\left(A\right)=0\vee O\left(A\right)\in \mathbb{N}\right)$$
10	6 9	syl	$$⊢A\in X\to \left(O\left(A\right)=0\vee O\left(A\right)\in \mathbb{N}\right)$$
11	10	orcomd	$$⊢A\in X\to \left(O\left(A\right)\in \mathbb{N}\vee O\left(A\right)=0\right)$$
12		elnn0	$$⊢O\left(A\right)\in {\mathbb{N}}_0\leftrightarrow \left(O\left(A\right)\in \mathbb{N}\vee O\left(A\right)=0\right)$$
13	11 12	sylibr	$$⊢A\in X\to O\left(A\right)\in {\mathbb{N}}_0$$