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 = ( Base ` G )
	odcl.2	|- O = ( od ` G )
Assertion	odcl	|- ( A e. X -> ( O ` A ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	|- X = ( Base ` G )
2		odcl.2	|- O = ( od ` G )
3		eqid	|- ( .g ` G ) = ( .g ` G )
4		eqid	|- ( 0g ` G ) = ( 0g ` G )
5		eqid	|- { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } = { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) }
6	1 3 4 2 5	odlem1	|- ( A e. X -> ( ( ( O ` A ) = 0 /\ { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } = (/) ) \/ ( O ` A ) e. { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } ) )
7		simpl	|- ( ( ( O ` A ) = 0 /\ { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } = (/) ) -> ( O ` A ) = 0 )
8		elrabi	|- ( ( O ` A ) e. { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } -> ( O ` A ) e. NN )
9	7 8	orim12i	|- ( ( ( ( O ` A ) = 0 /\ { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } = (/) ) \/ ( O ` A ) e. { y e. NN | ( y ( .g ` G ) A ) = ( 0g ` G ) } ) -> ( ( O ` A ) = 0 \/ ( O ` A ) e. NN ) )
10	6 9	syl	|- ( A e. X -> ( ( O ` A ) = 0 \/ ( O ` A ) e. NN ) )
11	10	orcomd	|- ( A e. X -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
12		elnn0	|- ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
13	11 12	sylibr	|- ( A e. X -> ( O ` A ) e. NN0 )