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 7 12 15 23 30 dvds2addd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) )
32 11 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐶 · 𝑥 ) ∈ ℂ )
33 14 zcnd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
34 19 32 33 adddid ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) = ( ( 𝐵 · ( 𝐶 · 𝑥 ) ) + ( 𝐵 · ( 𝐴 · 𝑦 ) ) ) )
35 31 34 breqtrrd ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∥ ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) )
36 oveq2 ⊢ ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) = ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) )
37 36 breq2d ⊢ ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ↔ 𝐴 ∥ ( 𝐵 · ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) ) ) )
38 35 37 syl5ibrcom ⊢ ( ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )
39 38 rexlimdvva ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝐶 gcd 𝐴 ) = ( ( 𝐶 · 𝑥 ) + ( 𝐴 · 𝑦 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )
40 6 39 mpd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · 𝐶 ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) )
41 dvdszrcl ⊢ ( 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ) )
42 41 adantl ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐴 ∈ ℤ ∧ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ ) )
43 42 simpld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∈ ℤ )
44 42 simprd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∈ ℤ )
45 zmulcl ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
46 45 adantr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · 𝐶 ) ∈ ℤ )
47 simpr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) )
48 simplr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐶 ∈ ℤ )
49 gcddvds ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐴 ) ∥ 𝐴 ) )
50 48 43 49 syl2anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝐴 ) ∥ 𝐴 ) )
51 50 simpld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∥ 𝐶 )
52 48 43 gcdcld ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∈ ℕ0 )
53 52 nn0zd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐶 gcd 𝐴 ) ∈ ℤ )
54 simpll ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐵 ∈ ℤ )
55 dvdscmul ⊢ ( ( ( 𝐶 gcd 𝐴 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) )
56 53 48 54 55 syl3anc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( ( 𝐶 gcd 𝐴 ) ∥ 𝐶 → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) ) )
57 51 56 mpd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ∥ ( 𝐵 · 𝐶 ) )
58 43 44 46 47 57 dvdstrd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) → 𝐴 ∥ ( 𝐵 · 𝐶 ) )
59 40 58 impbida ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∥ ( 𝐵 · 𝐶 ) ↔ 𝐴 ∥ ( 𝐵 · ( 𝐶 gcd 𝐴 ) ) ) )