Metamath Proof Explorer

Theorem dvdsmulgcd

Description: A divisibility equivalent for odmulg . (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion dvdsmulgcd ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 · 𝐶 ) ↔ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → 𝐶 ∈ ℤ )
2 dvdszrcl ⊢ ( 𝐴 ∥ ( 𝐵 · 𝐶 ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ) )
3 2 adantl ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ) )
4 3 simpld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → 𝐴 ∈ ℤ )
5 bezout ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) )
6 1 4 5 syl2anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) )
7 4 adantr ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
8 simplll ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
9 simpllr ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐶 ∈ ℤ )
10 simprl ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
11 9 10 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐶 · 𝑥 ) ∈ ℤ )
12 8 11 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · ( 𝐶 · 𝑥 ) ) ∈ ℤ )
13 simprr ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
14 7 13 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐴 · 𝑦 ) ∈ ℤ )
15 8 14 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · ( 𝐴 · 𝑦 ) ) ∈ ℤ )
16 8 9 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
17 simplr ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐵 · 𝐶 ) )
18 7 16 10 17 dvdsmultr1d ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( ( 𝐵 · 𝐶 ) · 𝑥 ) )
19 8 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐵 ∈ ℂ )
20 9 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐶 ∈ ℂ )
21 10 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℂ )
22 19 20 21 mulassd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝐵 · 𝐶 ) · 𝑥 ) = ( 𝐵 · ( 𝐶 · 𝑥 ) ) )
23 18 22 breqtrd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 · 𝑥 ) ) )
24 8 13 zmulcld ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · 𝑦 ) ∈ ℤ )
25 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · 𝑦 ) ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · ( 𝐵 · 𝑦 ) ) )
26 7 24 25 syl2anc ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐴 · ( 𝐵 · 𝑦 ) ) )
27 7 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ ℂ )
28 13 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
29 19 27 28 mul12d ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · ( 𝐴 · 𝑦 ) ) = ( 𝐴 · ( 𝐵 · 𝑦 ) ) )
30 26 29 breqtrrd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐴 · 𝑦 ) ) )
31 dvds2add ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 · 𝑥 ) ) ∈ ℤ ∧ ( 𝐵 · ( 𝐴 · 𝑦 ) ) ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 · ( 𝐶 · 𝑥 ) ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) → 𝐴 ∥ ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) ) )
32 31 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 · 𝑥 ) ) ∈ ℤ ∧ ( 𝐵 · ( 𝐴 · 𝑦 ) ) ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 · ( 𝐶 · 𝑥 ) ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) ) → 𝐴 ∥ ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) )
33 7 12 15 23 30 32 syl32anc ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) )
34 11 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐶 · 𝑥 ) ∈ ℂ )
35 14 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
36 19 34 35 adddid ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) = ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) )
37 33 36 breqtrrd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) )
38 oveq2 ⊢ ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) = ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) )
39 38 breq2d ⊢ ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ↔ 𝐴 ∥ ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) ) )
40 37 39 syl5ibrcom ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )
41 40 rexlimdvva ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )
42 6 41 mpd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) )
43 dvdszrcl ⊢ ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ) )
44 43 adantl ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ) )
45 44 simpld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∈ ℤ )
46 44 simprd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ )
47 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
48 47 adantr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
49 simpr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) )
50 simplr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐶 ∈ ℤ )
51 gcddvds ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐴 ) ∥ 𝐴 ) )
52 50 45 51 syl2anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐴 ) ∥ 𝐴 ) )
53 52 simpld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∥ 𝐶 )
54 50 45 gcdcld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∈ ℕ0 )
55 54 nn0zd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∈ ℤ )
56 simpll ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐵 ∈ ℤ )
57 dvdscmul ⊢ ( ( ( 𝐶 gcd 𝐴 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) )
58 55 50 56 57 syl3anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) )
59 53 58 mpd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) )
60 dvdstr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) → 𝐴 ∥ ( 𝐵 · 𝐶 ) ) )
61 60 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ∧ ( 𝐵 · 𝐶 ) ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) ) → 𝐴 ∥ ( 𝐵 · 𝐶 ) )
62 45 46 48 49 59 61 syl32anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∥ ( 𝐵 · 𝐶 ) )
63 42 62 impbida ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 · 𝐶 ) ↔ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )