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

Metamath Proof Explorer

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 )