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 ) )