Metamath Proof Explorer

Theorem dvdsmulgcd

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

Ref Expression
Assertion dvdsmulgcd ⊢ B ∈ ℤ ∧ C ∈ ℤ → A ∥ B ⁢ C ↔ A ∥ B ⁢ C gcd A

Proof

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