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