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 syl5bb
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` ( N .x. A ) ) = ( O ` A ) <-> ( N gcd ( O ` A ) ) = 1 ) )