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

Metamath Proof Explorer

Theorem oddvdsi

Description: Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 
|- X = ( Base ` G )
odcl.2 
|- O = ( od ` G )
odid.3 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
Assertion oddvdsi 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( N .x. A ) = .0. )

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 odid.3 
 |-  .x. = ( .g ` G )
4 odid.4 
 |-  .0. = ( 0g ` G )
5 simp3 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( O ` A ) || N )
6 dvdszrcl 
 |-  ( ( O ` A ) || N -> ( ( O ` A ) e. ZZ /\ N e. ZZ ) )
7 6 simprd 
 |-  ( ( O ` A ) || N -> N e. ZZ )
8 1 2 3 4 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
9 7 8 syl3an3 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
10 5 9 mpbid 
 |-  ( ( G e. Grp /\ A e. X /\ ( O ` A ) || N ) -> ( N .x. A ) = .0. )