This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odadd2

Description: The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (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 odadd2 
|- ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 odadd1.1 
 |-  O = ( od ` G )
2 odadd1.2 
 |-  X = ( Base ` G )
3 odadd1.3 
 |-  .+ = ( +g ` G )
4 2 1 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
5 4 3ad2ant2 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` A ) e. NN0 )
6 5 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` A ) e. ZZ )
7 2 1 odcl 
 |-  ( B e. X -> ( O ` B ) e. NN0 )
8 7 3ad2ant3 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` B ) e. NN0 )
9 8 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` B ) e. ZZ )
10 6 9 zmulcld 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) x. ( O ` B ) ) e. ZZ )
11 10 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) e. ZZ )
12 dvds0 
 |-  ( ( ( O ` A ) x. ( O ` B ) ) e. ZZ -> ( ( O ` A ) x. ( O ` B ) ) || 0 )
13 11 12 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) || 0 )
14 simpr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) = 0 )
15 14 sq0id 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) = 0 )
16 15 oveq2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = ( ( O ` ( A .+ B ) ) x. 0 ) )
17 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
18 2 3 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
19 17 18 syl3an1 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
20 2 1 odcl 
 |-  ( ( A .+ B ) e. X -> ( O ` ( A .+ B ) ) e. NN0 )
21 19 20 syl 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` ( A .+ B ) ) e. NN0 )
22 21 nn0zd 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( O ` ( A .+ B ) ) e. ZZ )
23 22 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( O ` ( A .+ B ) ) e. ZZ )
24 23 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( O ` ( A .+ B ) ) e. CC )
25 24 mul01d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. 0 ) = 0 )
26 16 25 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = 0 )
27 13 26 breqtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 0 ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
28 6 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) e. ZZ )
29 9 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) e. ZZ )
30 28 29 gcdcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) e. NN0 )
31 30 nn0cnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) e. CC )
32 31 sqvald 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) = ( ( ( O ` A ) gcd ( O ` B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
33 32 oveq2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) )
34 gcddvds 
 |-  ( ( ( O ` A ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) /\ ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) ) )
35 28 29 34 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 ) ) )
36 35 simpld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) || ( O ` A ) )
37 30 nn0zd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) e. ZZ )
38 simpr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) =/= 0 )
39 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 ) )
40 37 38 28 39 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 ) )
41 36 40 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 )
42 41 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. CC )
43 35 simprd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) gcd ( O ` B ) ) || ( O ` B ) )
44 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 ) )
45 37 38 29 44 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 ) )
46 43 45 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 )
47 46 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. CC )
48 42 31 47 31 mul4d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) = ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) )
49 28 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) e. CC )
50 49 31 38 divcan1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( O ` A ) )
51 29 zcnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) e. CC )
52 51 31 38 divcan1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( O ` B ) )
53 50 52 oveq12d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) = ( ( O ` A ) x. ( O ` B ) ) )
54 33 48 53 3eqtr2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = ( ( O ` A ) x. ( O ` B ) ) )
55 22 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) e. ZZ )
56 dvdsmul2 
 |-  ( ( ( O ` ( A .+ B ) ) e. ZZ /\ ( O ` A ) e. ZZ ) -> ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) )
57 55 28 56 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) )
58 simpl1 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> G e. Abel )
59 55 29 zmulcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ )
60 simpl2 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> A e. X )
61 simpl3 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> B e. X )
62 eqid 
 |-  ( .g ` G ) = ( .g ` G )
63 2 62 3 mulgdi 
 |-  ( ( G e. Abel /\ ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ /\ A e. X /\ B e. X ) ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) ) )
64 58 59 60 61 63 syl13anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) ) )
65 dvdsmul2 
 |-  ( ( ( O ` ( A .+ B ) ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) )
66 55 29 65 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) )
67 58 17 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> G e. Grp )
68 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
69 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ B e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ ) -> ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
70 67 61 59 69 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
71 66 70 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) = ( 0g ` G ) )
72 71 oveq2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( 0g ` G ) ) )
73 64 72 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( 0g ` G ) ) )
74 dvdsmul1 
 |-  ( ( ( O ` ( A .+ B ) ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) )
75 55 29 74 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) )
76 19 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( A .+ B ) e. X )
77 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ ( A .+ B ) e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ ) -> ( ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
78 67 76 59 77 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
79 75 78 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) )
80 2 62 mulgcl 
 |-  ( ( G e. Grp /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ /\ A e. X ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) e. X )
81 67 59 60 80 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) e. X )
82 2 3 68 grprid 
 |-  ( ( G e. Grp /\ ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) e. X ) -> ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( 0g ` G ) ) = ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) )
83 67 81 82 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) .+ ( 0g ` G ) ) = ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) )
84 73 79 83 3eqtr3rd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) = ( 0g ` G ) )
85 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ ) -> ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
86 67 60 59 85 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
87 84 86 mpbird 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) )
88 55 28 zmulcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ )
89 dvdsgcd 
 |-  ( ( ( O ` A ) e. ZZ /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ ) -> ( ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) /\ ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) -> ( O ` A ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) ) )
90 28 88 59 89 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) /\ ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) -> ( O ` A ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) ) )
91 57 87 90 mp2and 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) )
92 21 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) e. NN0 )
93 mulgcd 
 |-  ( ( ( O ` ( A .+ B ) ) e. NN0 /\ ( O ` A ) e. ZZ /\ ( O ` B ) e. ZZ ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) = ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
94 92 28 29 93 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) = ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
95 91 94 breqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
96 50 95 eqbrtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
97 dvdsmulcr 
 |-  ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( O ` ( A .+ B ) ) e. ZZ /\ ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) )
98 41 55 37 38 97 syl112anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) )
99 96 98 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) )
100 2 62 3 mulgdi 
 |-  ( ( G e. Abel /\ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ /\ A e. X /\ B e. X ) ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) )
101 58 88 60 61 100 syl13anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) )
102 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ ) -> ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
103 67 60 88 102 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) = ( 0g ` G ) ) )
104 57 103 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) = ( 0g ` G ) )
105 104 oveq1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) A ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) = ( ( 0g ` G ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) )
106 101 105 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( ( 0g ` G ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) )
107 dvdsmul1 
 |-  ( ( ( O ` ( A .+ B ) ) e. ZZ /\ ( O ` A ) e. ZZ ) -> ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) )
108 55 28 107 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) )
109 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ ( A .+ B ) e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ ) -> ( ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
110 67 76 88 109 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` ( A .+ B ) ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) ) )
111 108 110 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) ( A .+ B ) ) = ( 0g ` G ) )
112 2 62 mulgcl 
 |-  ( ( G e. Grp /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ /\ B e. X ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) e. X )
113 67 88 61 112 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) e. X )
114 2 3 68 grplid 
 |-  ( ( G e. Grp /\ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) e. X ) -> ( ( 0g ` G ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) = ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) )
115 67 113 114 syl2anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( 0g ` G ) .+ ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) ) = ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) )
116 106 111 115 3eqtr3rd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) = ( 0g ` G ) )
117 2 1 62 68 oddvds 
 |-  ( ( G e. Grp /\ B e. X /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ ) -> ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
118 67 61 88 117 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) <-> ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) ( .g ` G ) B ) = ( 0g ` G ) ) )
119 116 118 mpbird 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) )
120 dvdsgcd 
 |-  ( ( ( O ` B ) e. ZZ /\ ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) e. ZZ /\ ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) e. ZZ ) -> ( ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) /\ ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) -> ( O ` B ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) ) )
121 29 88 59 120 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) /\ ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) -> ( O ` B ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) ) )
122 119 66 121 mp2and 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( ( O ` ( A .+ B ) ) x. ( O ` A ) ) gcd ( ( O ` ( A .+ B ) ) x. ( O ` B ) ) ) )
123 122 94 breqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( O ` B ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
124 52 123 eqbrtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
125 dvdsmulcr 
 |-  ( ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( O ` ( A .+ B ) ) e. ZZ /\ ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) ) -> ( ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) )
126 46 55 37 38 125 syl112anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) <-> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) )
127 124 126 mpbid 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) )
128 41 46 gcdcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) e. NN0 )
129 128 nn0cnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) e. CC )
130 1cnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> 1 e. CC )
131 31 mullidd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( 1 x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` A ) gcd ( O ` B ) ) )
132 50 52 oveq12d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) = ( ( O ` A ) gcd ( O ` B ) ) )
133 mulgcdr 
 |-  ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( ( O ` A ) gcd ( O ` B ) ) e. NN0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) = ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
134 41 46 30 133 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) ) = ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) )
135 131 132 134 3eqtr2rd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( 1 x. ( ( O ` A ) gcd ( O ` B ) ) ) )
136 129 130 31 38 135 mulcan2ad 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) = 1 )
137 coprmdvds2 
 |-  ( ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) e. ZZ /\ ( O ` ( A .+ B ) ) e. ZZ ) /\ ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) gcd ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) = 1 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) /\ ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) || ( O ` ( A .+ B ) ) ) )
138 41 46 55 136 137 syl31anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) /\ ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) || ( O ` ( A .+ B ) ) ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) || ( O ` ( A .+ B ) ) ) )
139 99 127 138 mp2and 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) || ( O ` ( A .+ B ) ) )
140 41 46 zmulcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) e. ZZ )
141 zsqcl 
 |-  ( ( ( O ` A ) gcd ( O ` B ) ) e. ZZ -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) e. ZZ )
142 37 141 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) e. ZZ )
143 dvdsmulc 
 |-  ( ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) e. ZZ /\ ( O ` ( A .+ B ) ) e. ZZ /\ ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) e. ZZ ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) || ( O ` ( A .+ B ) ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) ) )
144 140 55 142 143 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) || ( O ` ( A .+ B ) ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) ) )
145 139 144 mpd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( ( ( O ` A ) / ( ( O ` A ) gcd ( O ` B ) ) ) x. ( ( O ` B ) / ( ( O ` A ) gcd ( O ` B ) ) ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
146 54 145 eqbrtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) =/= 0 ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
147 27 146 pm2.61dane 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )