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

Metamath Proof Explorer

Theorem odmulg2

Description: The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 
|- X = ( Base ` G )
odmulgid.2 
|- O = ( od ` G )
odmulgid.3 
|- .x. = ( .g ` G )
Assertion odmulg2 
|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 
 |-  X = ( Base ` G )
2 odmulgid.2 
 |-  O = ( od ` G )
3 odmulgid.3 
 |-  .x. = ( .g ` G )
4 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
5 4 nn0zd 
 |-  ( A e. X -> ( O ` A ) e. ZZ )
6 5 3ad2ant2 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) e. ZZ )
7 simp3 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> N e. ZZ )
8 dvdsmul1 
 |-  ( ( ( O ` A ) e. ZZ /\ N e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. N ) )
9 6 7 8 syl2anc 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. N ) )
10 1 2 3 odmulgid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. ZZ ) -> ( ( O ` ( N .x. A ) ) || ( O ` A ) <-> ( O ` A ) || ( ( O ` A ) x. N ) ) )
11 6 10 mpdan 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` ( N .x. A ) ) || ( O ` A ) <-> ( O ` A ) || ( ( O ` A ) x. N ) ) )
12 9 11 mpbird 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )