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