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

Metamath Proof Explorer

Theorem odmulgeq

Description: A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 odmulgid.1 
 |-  X = ( Base ` G )
2 odmulgid.2 
 |-  O = ( od ` G )
3 odmulgid.3 
 |-  .x. = ( .g ` G )
4 eqcom 
 |-  ( ( O ` ( N .x. A ) ) = ( O ` A ) <-> ( O ` A ) = ( O ` ( N .x. A ) ) )
5 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> A e. X )
6 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
7 5 6 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN0 )
8 7 nn0cnd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. CC )
9 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> G e. Grp )
10 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> N e. ZZ )
11 1 3 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( N .x. A ) e. X )
12 9 10 5 11 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N .x. A ) e. X )
13 1 2 odcl 
 |-  ( ( N .x. A ) e. X -> ( O ` ( N .x. A ) ) e. NN0 )
14 12 13 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` ( N .x. A ) ) e. NN0 )
15 14 nn0cnd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` ( N .x. A ) ) e. CC )
16 nnne0 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) =/= 0 )
17 16 adantl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) =/= 0 )
18 1 2 3 odmulg2 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )
19 18 adantr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` ( N .x. A ) ) || ( O ` A ) )
20 breq1 
 |-  ( ( O ` ( N .x. A ) ) = 0 -> ( ( O ` ( N .x. A ) ) || ( O ` A ) <-> 0 || ( O ` A ) ) )
21 19 20 syl5ibcom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) = 0 -> 0 || ( O ` A ) ) )
22 7 nn0zd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. ZZ )
23 0dvds 
 |-  ( ( O ` A ) e. ZZ -> ( 0 || ( O ` A ) <-> ( O ` A ) = 0 ) )
24 22 23 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( 0 || ( O ` A ) <-> ( O ` A ) = 0 ) )
25 21 24 sylibd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) = 0 -> ( O ` A ) = 0 ) )
26 25 necon3d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) =/= 0 -> ( O ` ( N .x. A ) ) =/= 0 ) )
27 17 26 mpd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` ( N .x. A ) ) =/= 0 )
28 8 15 27 diveq1ad 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) / ( O ` ( N .x. A ) ) ) = 1 <-> ( O ` A ) = ( O ` ( N .x. A ) ) ) )
29 10 22 gcdcld 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N gcd ( O ` A ) ) e. NN0 )
30 29 nn0cnd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N gcd ( O ` A ) ) e. CC )
31 15 30 mulcomd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) x. ( N gcd ( O ` A ) ) ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
32 1 2 3 odmulg 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
33 32 adantr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
34 31 33 eqtr4d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) x. ( N gcd ( O ` A ) ) ) = ( O ` A ) )
35 8 15 30 27 divmuld 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) / ( O ` ( N .x. A ) ) ) = ( N gcd ( O ` A ) ) <-> ( ( O ` ( N .x. A ) ) x. ( N gcd ( O ` A ) ) ) = ( O ` A ) ) )
36 34 35 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) / ( O ` ( N .x. A ) ) ) = ( N gcd ( O ` A ) ) )
37 36 eqeq1d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) / ( O ` ( N .x. A ) ) ) = 1 <-> ( N gcd ( O ` A ) ) = 1 ) )
38 28 37 bitr3d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) = ( O ` ( N .x. A ) ) <-> ( N gcd ( O ` A ) ) = 1 ) )
39 4 38 bitrid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) = ( O ` A ) <-> ( N gcd ( O ` A ) ) = 1 ) )