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 ⊢ 𝑂 = ( 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 mullidd ⊢ ( ( ( 𝐺 ∈ 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 ) ) )