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

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

Proof

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