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