bezout

Description: Bézout's identity: For any integers A and B , there are integers x , y such that ( A gcd B ) = A x. x + B x. y . This is Metamath 100 proof #60. (Contributed by Mario Carneiro, 22-Feb-2014)

		Ref	Expression
	Assertion	bezout	$⊢ (A \in ℤ \land B \in ℤ) \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ z = t \to (z = A x + B y \leftrightarrow t = A x + B y)$
2	1	2rexbidv	$⊢ z = t \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ t = A x + B y)$
3		oveq2	$⊢ x = u \to A x = A u$
4	3	oveq1d	$⊢ x = u \to A x + B y = A u + B y$
5	4	eqeq2d	$⊢ x = u \to (t = A x + B y \leftrightarrow t = A u + B y)$
6		oveq2	$⊢ y = v \to B y = B v$
7	6	oveq2d	$⊢ y = v \to A u + B y = A u + B v$
8	7	eqeq2d	$⊢ y = v \to (t = A u + B y \leftrightarrow t = A u + B v)$
9	5 8	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ t = A x + B y \leftrightarrow \exists u \in ℤ \exists v \in ℤ t = A u + B v$
10	2 9	bitrdi	$⊢ z = t \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists u \in ℤ \exists v \in ℤ t = A u + B v)$
11	10	cbvrabv	$⊢ \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} = \{t \in ℕ \| \exists u \in ℤ \exists v \in ℤ t = A u + B v\}$
12		simpll	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \in ℤ$
13		simplr	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to B \in ℤ$
14		eqid	$⊢ sup (\{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} ℝ <) = sup (\{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} ℝ <)$
15		simpr	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to \neg (A = 0 \land B = 0)$
16	11 12 13 14 15	bezoutlem4	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\}$
17		eqeq1	$⊢ z = A \gcd B \to (z = A x + B y \leftrightarrow A \gcd B = A x + B y)$
18	17	2rexbidv	$⊢ z = A \gcd B \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y)$
19	18	elrab	$⊢ A \gcd B \in \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} \leftrightarrow (A \gcd B \in ℕ \land \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y)$
20	19	simprbi	$⊢ A \gcd B \in \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y$
21	16 20	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y$
22	21	ex	$⊢ (A \in ℤ \land B \in ℤ) \to (\neg (A = 0 \land B = 0) \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y)$
23		0z	$⊢ 0 \in ℤ$
24		00id	$⊢ 0 + 0 = 0$
25		0cn	$⊢ 0 \in ℂ$
26	25	mul01i	$⊢ 0 \cdot 0 = 0$
27	26 26	oveq12i	$⊢ 0 \cdot 0 + 0 \cdot 0 = 0 + 0$
28		gcd0val	$⊢ 0 \gcd 0 = 0$
29	24 27 28	3eqtr4ri	$⊢ 0 \gcd 0 = 0 \cdot 0 + 0 \cdot 0$
30		oveq2	$⊢ x = 0 \to 0 \cdot x = 0 \cdot 0$
31	30	oveq1d	$⊢ x = 0 \to 0 \cdot x + 0 \cdot y = 0 \cdot 0 + 0 \cdot y$
32	31	eqeq2d	$⊢ x = 0 \to (0 \gcd 0 = 0 \cdot x + 0 \cdot y \leftrightarrow 0 \gcd 0 = 0 \cdot 0 + 0 \cdot y)$
33		oveq2	$⊢ y = 0 \to 0 \cdot y = 0 \cdot 0$
34	33	oveq2d	$⊢ y = 0 \to 0 \cdot 0 + 0 \cdot y = 0 \cdot 0 + 0 \cdot 0$
35	34	eqeq2d	$⊢ y = 0 \to (0 \gcd 0 = 0 \cdot 0 + 0 \cdot y \leftrightarrow 0 \gcd 0 = 0 \cdot 0 + 0 \cdot 0)$
36	32 35	rspc2ev	$⊢ (0 \in ℤ \land 0 \in ℤ \land 0 \gcd 0 = 0 \cdot 0 + 0 \cdot 0) \to \exists x \in ℤ \exists y \in ℤ 0 \gcd 0 = 0 \cdot x + 0 \cdot y$
37	23 23 29 36	mp3an	$⊢ \exists x \in ℤ \exists y \in ℤ 0 \gcd 0 = 0 \cdot x + 0 \cdot y$
38		oveq12	$⊢ (A = 0 \land B = 0) \to A \gcd B = 0 \gcd 0$
39		oveq1	$⊢ A = 0 \to A x = 0 \cdot x$
40		oveq1	$⊢ B = 0 \to B y = 0 \cdot y$
41	39 40	oveqan12d	$⊢ (A = 0 \land B = 0) \to A x + B y = 0 \cdot x + 0 \cdot y$
42	38 41	eqeq12d	$⊢ (A = 0 \land B = 0) \to (A \gcd B = A x + B y \leftrightarrow 0 \gcd 0 = 0 \cdot x + 0 \cdot y)$
43	42	2rexbidv	$⊢ (A = 0 \land B = 0) \to (\exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ 0 \gcd 0 = 0 \cdot x + 0 \cdot y)$
44	37 43	mpbiri	$⊢ (A = 0 \land B = 0) \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y$
45	22 44	pm2.61d2	$⊢ (A \in ℤ \land B \in ℤ) \to \exists x \in ℤ \exists y \in ℤ A \gcd B = A x + B y$

Metamath Proof Explorer

Theorem bezout

Proof