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 ) ) ) )