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	$⊢ ((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \to (A X + B Y = 1 \to A \gcd B = 1)$

Proof

Step	Hyp	Ref	Expression
1		bezoutr	$⊢ ((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \to (A \gcd B) ∥ (A X + B Y)$
2	1	adantr	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to (A \gcd B) ∥ (A X + B Y)$
3		simpr	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to A X + B Y = 1$
4	2 3	breqtrd	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to (A \gcd B) ∥ 1$
5		gcdcl	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℕ_{0}$
6	5	nn0zd	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℤ$
7	6	ad2antrr	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to A \gcd B \in ℤ$
8		1nn	$⊢ 1 \in ℕ$
9	8	a1i	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to 1 \in ℕ$
10		dvdsle	$⊢ (A \gcd B \in ℤ \land 1 \in ℕ) \to ((A \gcd B) ∥ 1 \to A \gcd B \leq 1)$
11	7 9 10	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to ((A \gcd B) ∥ 1 \to A \gcd B \leq 1)$
12	4 11	mpd	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to A \gcd B \leq 1$
13		simpll	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to (A \in ℤ \land B \in ℤ)$
14		oveq1	$⊢ A = 0 \to A X = 0 \cdot X$
15		oveq1	$⊢ B = 0 \to B Y = 0 \cdot Y$
16	14 15	oveqan12d	$⊢ (A = 0 \land B = 0) \to A X + B Y = 0 \cdot X + 0 \cdot Y$
17		zcn	$⊢ X \in ℤ \to X \in ℂ$
18	17	mul02d	$⊢ X \in ℤ \to 0 \cdot X = 0$
19		zcn	$⊢ Y \in ℤ \to Y \in ℂ$
20	19	mul02d	$⊢ Y \in ℤ \to 0 \cdot Y = 0$
21	18 20	oveqan12d	$⊢ (X \in ℤ \land Y \in ℤ) \to 0 \cdot X + 0 \cdot Y = 0 + 0$
22	16 21	sylan9eqr	$⊢ ((X \in ℤ \land Y \in ℤ) \land (A = 0 \land B = 0)) \to A X + B Y = 0 + 0$
23		00id	$⊢ 0 + 0 = 0$
24	22 23	syl6eq	$⊢ ((X \in ℤ \land Y \in ℤ) \land (A = 0 \land B = 0)) \to A X + B Y = 0$
25	24	adantll	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land (A = 0 \land B = 0)) \to A X + B Y = 0$
26		0ne1	$⊢ 0 \neq 1$
27	26	a1i	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land (A = 0 \land B = 0)) \to 0 \neq 1$
28	25 27	eqnetrd	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land (A = 0 \land B = 0)) \to A X + B Y \neq 1$
29	28	ex	$⊢ ((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \to ((A = 0 \land B = 0) \to A X + B Y \neq 1)$
30	29	necon2bd	$⊢ ((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \to (A X + B Y = 1 \to \neg (A = 0 \land B = 0))$
31	30	imp	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to \neg (A = 0 \land B = 0)$
32		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
33	13 31 32	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to A \gcd B \in ℕ$
34		nnle1eq1	$⊢ A \gcd B \in ℕ \to (A \gcd B \leq 1 \leftrightarrow A \gcd B = 1)$
35	33 34	syl	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to (A \gcd B \leq 1 \leftrightarrow A \gcd B = 1)$
36	12 35	mpbid	$⊢ (((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \land A X + B Y = 1) \to A \gcd B = 1$
37	36	ex	$⊢ ((A \in ℤ \land B \in ℤ) \land (X \in ℤ \land Y \in ℤ)) \to (A X + B Y = 1 \to A \gcd B = 1)$

Metamath Proof Explorer

Theorem bezoutr1

Proof