This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )