This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )