Metamath Proof Explorer

Theorem odadd1

Description: The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses odadd1.1 
|- O = ( od ` G )
odadd1.2 
|- X = ( Base ` G )
odadd1.3 
|- .+ = ( +g ` G )
Assertion odadd1 
|- ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )

Proof

Step Hyp Ref Expression
1 odadd1.1 
 |-  O = ( od ` G )
2 odadd1.2 
 |-  X = ( Base ` G )
3 odadd1.3 
 |-  .+ = ( +g ` G )
4 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
5 2 3 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
6 4 5 syl3an1 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
7 2 1 odcl 
 |-  ( ( A .+ B ) e. X -> ( O ` ( A .+ B ) ) e. NN0 )
8 6 7 syl 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` ( A .+ B ) ) e. NN0 )
9 8 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` ( A .+ B ) ) e. ZZ )
10 2 1 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
11 10 3ad2ant2 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` A ) e. NN0 )
12 11 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` A ) e. ZZ )
13 2 1 odcl 
 |-  ( B e. X -> ( O ` B ) e. NN0 )
14 13 3ad2ant3 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` B ) e. NN0 )
15 14 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` B ) e. ZZ )
16 12 15 gcdcld 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) gcd ( O ` B ) ) e. NN0 )
17 16 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) gcd ( O ` B ) ) e. ZZ )
18 9 17 zmulcld 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ )
19 18 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ )
20 dvds0 
 |-  ( ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || 0 )
21 19 20 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || 0 )
22 gcdeq0 
 |-  ( ( ( O ` A ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) = 0 <-> ( ( O ` A ) = 0 /\ ( O ` B ) = 0 ) ) )
23 12 15 22 syl2anc 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( ( O ` A ) gcd ( O ` B ) ) = 0 <-> ( ( O ` A ) = 0 /\ ( O ` B ) = 0 ) ) )
24 23 biimpa 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) = 0 /\ ( O ` B ) = 0 ) )
25 oveq12 
 |-  ( ( ( O ` A ) = 0 /\ ( O ` B ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) = ( 0 x. 0 ) )
26 0cn 
 |-  0 e. CC
27 26 mul01i 
 |-  ( 0 x. 0 ) = 0
28 25 27 eqtrdi 
 |-  ( ( ( O ` A ) = 0 /\ ( O ` B ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) = 0 )
29 24 28 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) = 0 )
30 21 29 breqtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )
31 simpl1 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> G e. Abel )
32 17 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) e. ZZ )
33 12 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) e. ZZ )
34 15 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) e. ZZ )
35 gcddvds 
 |-  ( ( ( O ` A ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) /\ ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) /\ ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) ) )
37 36 simpld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) )
38 32 33 34 37 dvdsmultr1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) || ( ( O ` A ) x. ( O ` B ) ) )
39 simpr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) =/= 0 )
40 33 34 zmulcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) x. ( O ` B ) ) e. ZZ )
41 dvdsval2 
 |-  ( ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 /\ ( ( O ` A ) x. ( O ` B ) ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( ( O ` A ) x. ( O ` B ) ) <-> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
42 32 39 40 41 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( ( O ` A ) x. ( O ` B ) ) <-> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
43 38 42 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ )
44 simpl2 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> A e. X )
45 simpl3 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> B e. X )
46 eqid 
 |-  ( .g ` G ) = ( .g ` G )
47 2 46 3 mulgdi 
 |-  ( ( G e. Abel /\ ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ A e. X /\ B e. X ) ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) .+ ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) ) )
48 31 43 44 45 47 syl13anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) .+ ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) ) )
49 36 simprd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) )
50 dvdsval2 
 |-  ( ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 /\ ( O ` B ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) <-> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
51 32 39 34 50 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) <-> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
52 49 51 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ )
53 dvdsmul1 
 |-  ( ( ( O ` A ) e. ZZ /\ ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
54 33 52 53 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( O ` A ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
55 33 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) e. CC )
56 34 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) e. CC )
57 32 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) e. CC )
58 55 56 57 39 divassd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` A ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
59 54 58 breqtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) )
60 31 4 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> G e. Grp )
61 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
62 2 1 46 61 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) -> ( ( O ` A ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
63 60 44 43 62 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
64 59 63 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) = ( 0g ` G ) )
65 dvdsval2 
 |-  ( ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 /\ ( O ` A ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) <-> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
66 32 39 33 65 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) <-> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) )
67 37 66 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ )
68 dvdsmul1 
 |-  ( ( ( O ` B ) e. ZZ /\ ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) -> ( O ` B ) || ( ( O ` B ) x. ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
69 34 67 68 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( O ` B ) x. ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
70 55 56 mulcomd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) x. ( O ` B ) ) = ( ( O ` B ) x. ( O ` A ) ) )
71 70 oveq1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( ( O ` B ) x. ( O ` A ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) )
72 56 55 57 39 divassd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` B ) x. ( O ` A ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` B ) x. ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
73 71 72 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` B ) x. ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
74 69 73 breqtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) )
75 2 1 46 61 oddvds 
 |-  ( ( G e. Grp /\ B e. X /\ ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) -> ( ( O ` B ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
76 60 45 43 75 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
77 74 76 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) = ( 0g ` G ) )
78 64 77 oveq12d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) A ) .+ ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) B ) ) = ( ( 0g ` G ) .+ ( 0g ` G ) ) )
79 2 61 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
80 2 3 61 grplid 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. X ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
81 60 79 80 syl2anc2 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( 0g ` G ) .+ ( 0g ` G ) ) = ( 0g ` G ) )
82 48 78 81 3eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) )
83 6 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( A .+ B ) e. X )
84 2 1 46 61 oddvds 
 |-  ( ( G e. Grp /\ ( A .+ B ) e. X /\ ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ ) -> ( ( O ` ( A .+ B ) ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
85 60 83 43 84 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
86 82 85 mpbird 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) )
87 9 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) e. ZZ )
88 dvdsmulcr 
 |-  ( ( ( O ` ( A .+ B ) ) e. ZZ /\ ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) ) -> ( ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( O ` ( A .+ B ) ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
89 87 43 32 39 88 syl112anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( O ` ( A .+ B ) ) || ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) )
90 86 89 mpbird 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
91 40 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) x. ( O ` B ) ) e. CC )
92 91 57 39 divcan1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) x. ( O ` B ) ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` A ) x. ( O ` B ) ) )
93 90 92 breqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )
94 30 93 pm2.61dane 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )