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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	odcld.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion	odcld	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		odcld.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		odcld.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
4	1 2	odcl	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
5	3 4	syl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )