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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
2 1 nn0zd ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
3 2 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
4 simpll ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
5 simprl ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝑋 ∈ ℤ )
6 4 5 zmulcld ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 · 𝑋 ) ∈ ℤ )
7 simplr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
8 simprr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → 𝑌 ∈ ℤ )
9 7 8 zmulcld ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐵 · 𝑌 ) ∈ ℤ )
10 gcddvds ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
11 10 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
12 11 simpld ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
13 3 4 5 12 dvdsmultr1d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( 𝐴 · 𝑋 ) )
14 11 simprd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐵 )
15 3 7 8 14 dvdsmultr1d ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( 𝐵 · 𝑌 ) )
16 3 6 9 13 15 dvds2addd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )