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 𝑂 = ( od ‘ 𝐺 )
odadd1.2 𝑋 = ( Base ‘ 𝐺 )
odadd1.3 + = ( +g𝐺 )
Assertion odadd2 ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∥ ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) ) )

Proof

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