Metamath Proof Explorer

Theorem bezoutr

Description: Partial converse to bezout . Existence of a linear combination does not set the gcd, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion bezoutr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ A ⁢ X + B ⁢ Y

Proof

Step Hyp Ref Expression
1 gcdcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∈ ℕ 0
2 1 nn0zd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∈ ℤ
3 2 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∈ ℤ
4 simpll ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A ∈ ℤ
5 simprl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → X ∈ ℤ
6 4 5 zmulcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A ⁢ X ∈ ℤ
7 simplr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → B ∈ ℤ
8 simprr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → Y ∈ ℤ
9 7 8 zmulcld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → B ⁢ Y ∈ ℤ
10 gcddvds ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
11 10 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ A ∧ A gcd B ∥ B
12 11 simpld ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ A
13 3 4 5 12 dvdsmultr1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ A ⁢ X
14 11 simprd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ B
15 3 7 8 14 dvdsmultr1d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ B ⁢ Y
16 3 6 9 13 15 dvds2addd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ X ∈ ℤ ∧ Y ∈ ℤ → A gcd B ∥ A ⁢ X + B ⁢ Y