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

Metamath Proof Explorer

Theorem bezoutr1

Description: Converse of bezout for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion bezoutr1 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 → ( 𝐴 gcd 𝐵 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 bezoutr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )
2 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) ∥ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )
3 simpr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 )
4 2 3 breqtrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) ∥ 1 )
5 gcdcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
6 5 nn0zd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
7 6 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
8 1nn ⊢ 1 ∈ ℕ
9 8 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → 1 ∈ ℕ )
10 dvdsle ⊢ ( ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 1 → ( 𝐴 gcd 𝐵 ) ≤ 1 ) )
11 7 9 10 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( ( 𝐴 gcd 𝐵 ) ∥ 1 → ( 𝐴 gcd 𝐵 ) ≤ 1 ) )
12 4 11 mpd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) ≤ 1 )
13 simpll ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
14 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
15 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 · 𝑌 ) = ( 0 · 𝑌 ) )
16 14 15 oveqan12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 0 · 𝑋 ) + ( 0 · 𝑌 ) ) )
17 zcn ⊢ ( 𝑋 ∈ ℤ → 𝑋 ∈ ℂ )
18 17 mul02d ⊢ ( 𝑋 ∈ ℤ → ( 0 · 𝑋 ) = 0 )
19 zcn ⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℂ )
20 19 mul02d ⊢ ( 𝑌 ∈ ℤ → ( 0 · 𝑌 ) = 0 )
21 18 20 oveqan12d ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( 0 · 𝑋 ) + ( 0 · 𝑌 ) ) = ( 0 + 0 ) )
22 16 21 sylan9eqr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( 0 + 0 ) )
23 00id ⊢ ( 0 + 0 ) = 0
24 22 23 eqtrdi ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 0 )
25 24 adantll ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 0 )
26 0ne1 ⊢ 0 ≠ 1
27 26 a1i ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → 0 ≠ 1 )
28 25 27 eqnetrd ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ≠ 1 )
29 28 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ≠ 1 ) )
30 29 necon2bd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) )
31 30 imp ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
32 gcdn0cl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
33 13 31 32 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
34 nnle1eq1 ⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) ≤ 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
35 33 34 syl ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( ( 𝐴 gcd 𝐵 ) ≤ 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) )
36 12 35 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 )
37 36 ex ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ) → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 1 → ( 𝐴 gcd 𝐵 ) = 1 ) )