Metamath Proof Explorer


Theorem odmulg

Description: Relationship between the order of an element and that of a multiple. (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 odmulg
|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. 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 3 mulgcl
 |-  ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( N .x. A ) e. X )
5 4 3com23
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( N .x. A ) e. X )
6 1 2 odcl
 |-  ( ( N .x. A ) e. X -> ( O ` ( N .x. A ) ) e. NN0 )
7 5 6 syl
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) e. NN0 )
8 7 nn0cnd
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) e. CC )
9 8 adantr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( O ` ( N .x. A ) ) e. CC )
10 9 mul02d
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( 0 x. ( O ` ( N .x. A ) ) ) = 0 )
11 simpr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( N gcd ( O ` A ) ) = 0 )
12 11 oveq1d
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) = ( 0 x. ( O ` ( N .x. A ) ) ) )
13 simp3
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> N e. ZZ )
14 1 2 odcl
 |-  ( A e. X -> ( O ` A ) e. NN0 )
15 14 3ad2ant2
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) e. NN0 )
16 15 nn0zd
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) e. ZZ )
17 gcdeq0
 |-  ( ( N e. ZZ /\ ( O ` A ) e. ZZ ) -> ( ( N gcd ( O ` A ) ) = 0 <-> ( N = 0 /\ ( O ` A ) = 0 ) ) )
18 13 16 17 syl2anc
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( N gcd ( O ` A ) ) = 0 <-> ( N = 0 /\ ( O ` A ) = 0 ) ) )
19 18 simplbda
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( O ` A ) = 0 )
20 10 12 19 3eqtr4rd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 0 ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
21 simpll3
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> N e. ZZ )
22 16 ad2antrr
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( O ` A ) e. ZZ )
23 gcddvds
 |-  ( ( N e. ZZ /\ ( O ` A ) e. ZZ ) -> ( ( N gcd ( O ` A ) ) || N /\ ( N gcd ( O ` A ) ) || ( O ` A ) ) )
24 21 22 23 syl2anc
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( N gcd ( O ` A ) ) || N /\ ( N gcd ( O ` A ) ) || ( O ` A ) ) )
25 24 simprd
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( N gcd ( O ` A ) ) || ( O ` A ) )
26 13 16 gcdcld
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( N gcd ( O ` A ) ) e. NN0 )
27 26 adantr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( N gcd ( O ` A ) ) e. NN0 )
28 27 nn0zd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( N gcd ( O ` A ) ) e. ZZ )
29 28 adantr
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( N gcd ( O ` A ) ) e. ZZ )
30 nn0z
 |-  ( x e. NN0 -> x e. ZZ )
31 30 adantl
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> x e. ZZ )
32 dvdstr
 |-  ( ( ( N gcd ( O ` A ) ) e. ZZ /\ ( O ` A ) e. ZZ /\ x e. ZZ ) -> ( ( ( N gcd ( O ` A ) ) || ( O ` A ) /\ ( O ` A ) || x ) -> ( N gcd ( O ` A ) ) || x ) )
33 29 22 31 32 syl3anc
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( ( N gcd ( O ` A ) ) || ( O ` A ) /\ ( O ` A ) || x ) -> ( N gcd ( O ` A ) ) || x ) )
34 25 33 mpand
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( O ` A ) || x -> ( N gcd ( O ` A ) ) || x ) )
35 7 nn0zd
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` ( N .x. A ) ) e. ZZ )
36 35 ad2antrr
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( O ` ( N .x. A ) ) e. ZZ )
37 muldvds1
 |-  ( ( ( N gcd ( O ` A ) ) e. ZZ /\ ( O ` ( N .x. A ) ) e. ZZ /\ x e. ZZ ) -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x -> ( N gcd ( O ` A ) ) || x ) )
38 29 36 31 37 syl3anc
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x -> ( N gcd ( O ` A ) ) || x ) )
39 dvdszrcl
 |-  ( ( N gcd ( O ` A ) ) || x -> ( ( N gcd ( O ` A ) ) e. ZZ /\ x e. ZZ ) )
40 divides
 |-  ( ( ( N gcd ( O ` A ) ) e. ZZ /\ x e. ZZ ) -> ( ( N gcd ( O ` A ) ) || x <-> E. y e. ZZ ( y x. ( N gcd ( O ` A ) ) ) = x ) )
41 39 40 syl
 |-  ( ( N gcd ( O ` A ) ) || x -> ( ( N gcd ( O ` A ) ) || x <-> E. y e. ZZ ( y x. ( N gcd ( O ` A ) ) ) = x ) )
42 41 ibi
 |-  ( ( N gcd ( O ` A ) ) || x -> E. y e. ZZ ( y x. ( N gcd ( O ` A ) ) ) = x )
43 35 adantr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( O ` ( N .x. A ) ) e. ZZ )
44 simprr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> y e. ZZ )
45 28 adantrr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( N gcd ( O ` A ) ) e. ZZ )
46 simprl
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( N gcd ( O ` A ) ) =/= 0 )
47 dvdscmulr
 |-  ( ( ( O ` ( N .x. A ) ) e. ZZ /\ y e. ZZ /\ ( ( N gcd ( O ` A ) ) e. ZZ /\ ( N gcd ( O ` A ) ) =/= 0 ) ) -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( ( N gcd ( O ` A ) ) x. y ) <-> ( O ` ( N .x. A ) ) || y ) )
48 43 44 45 46 47 syl112anc
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( ( N gcd ( O ` A ) ) x. y ) <-> ( O ` ( N .x. A ) ) || y ) )
49 1 2 3 odmulgid
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ y e. ZZ ) -> ( ( O ` ( N .x. A ) ) || y <-> ( O ` A ) || ( y x. N ) ) )
50 49 adantrl
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( O ` ( N .x. A ) ) || y <-> ( O ` A ) || ( y x. N ) ) )
51 simpl3
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> N e. ZZ )
52 dvdsmulgcd
 |-  ( ( y e. ZZ /\ N e. ZZ ) -> ( ( O ` A ) || ( y x. N ) <-> ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) ) )
53 44 51 52 syl2anc
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( O ` A ) || ( y x. N ) <-> ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) ) )
54 48 50 53 3bitrrd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( ( N gcd ( O ` A ) ) x. y ) ) )
55 45 zcnd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( N gcd ( O ` A ) ) e. CC )
56 44 zcnd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> y e. CC )
57 55 56 mulcomd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( N gcd ( O ` A ) ) x. y ) = ( y x. ( N gcd ( O ` A ) ) ) )
58 57 breq2d
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( ( N gcd ( O ` A ) ) x. y ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( y x. ( N gcd ( O ` A ) ) ) ) )
59 54 58 bitrd
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( ( N gcd ( O ` A ) ) =/= 0 /\ y e. ZZ ) ) -> ( ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( y x. ( N gcd ( O ` A ) ) ) ) )
60 59 anassrs
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ y e. ZZ ) -> ( ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( y x. ( N gcd ( O ` A ) ) ) ) )
61 breq2
 |-  ( ( y x. ( N gcd ( O ` A ) ) ) = x -> ( ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( O ` A ) || x ) )
62 breq2
 |-  ( ( y x. ( N gcd ( O ` A ) ) ) = x -> ( ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) )
63 61 62 bibi12d
 |-  ( ( y x. ( N gcd ( O ` A ) ) ) = x -> ( ( ( O ` A ) || ( y x. ( N gcd ( O ` A ) ) ) <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || ( y x. ( N gcd ( O ` A ) ) ) ) <-> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
64 60 63 syl5ibcom
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ y e. ZZ ) -> ( ( y x. ( N gcd ( O ` A ) ) ) = x -> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
65 64 rexlimdva
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( E. y e. ZZ ( y x. ( N gcd ( O ` A ) ) ) = x -> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
66 42 65 syl5
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( ( N gcd ( O ` A ) ) || x -> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
67 66 adantr
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( N gcd ( O ` A ) ) || x -> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
68 34 38 67 pm5.21ndd
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) /\ x e. NN0 ) -> ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) )
69 68 ralrimiva
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> A. x e. NN0 ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) )
70 15 adantr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( O ` A ) e. NN0 )
71 7 adantr
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( O ` ( N .x. A ) ) e. NN0 )
72 27 71 nn0mulcld
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) e. NN0 )
73 dvdsext
 |-  ( ( ( O ` A ) e. NN0 /\ ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) e. NN0 ) -> ( ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) <-> A. x e. NN0 ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
74 70 72 73 syl2anc
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) <-> A. x e. NN0 ( ( O ` A ) || x <-> ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) || x ) ) )
75 69 74 mpbird
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) =/= 0 ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )
76 20 75 pm2.61dane
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) = ( ( N gcd ( O ` A ) ) x. ( O ` ( N .x. A ) ) ) )