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 = ( Base ` G )
	odcld.2	|- O = ( od ` G )
	odcld.3	|- ( ph -> A e. B )
Assertion	odcld	|- ( ph -> ( O ` A ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		odcld.1	|- B = ( Base ` G )
2		odcld.2	|- O = ( od ` G )
3		odcld.3	|- ( ph -> A e. B )
4	1 2	odcl	|- ( A e. B -> ( O ` A ) e. NN0 )
5	3 4	syl	|- ( ph -> ( O ` A ) e. NN0 )