Theorem odcld

Description: The order of a group element is always a nonnegative integer, deduction form of odcl . (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		odcld.1	$$⊢B={\mathrm{Base}}_G$$
2		odcld.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odcld.3	$$⊢\phi \to A\in B$$
4	1 2	odcl	$$⊢A\in B\to O\left(A\right)\in {\mathbb{N}}_0$$
5	3 4	syl	$$⊢\phi \to O\left(A\right)\in {\mathbb{N}}_0$$