# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}$

### Proof

Step Hyp Ref Expression
1 eqeq1 ${⊢}{z}={t}\to \left({z}={A}{x}+{B}{y}↔{t}={A}{x}+{B}{y}\right)$
2 1 2rexbidv ${⊢}{z}={t}\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{t}={A}{x}+{B}{y}\right)$
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 \left({t}={A}{x}+{B}{y}↔{t}={A}{u}+{B}{y}\right)$
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 \left({t}={A}{u}+{B}{y}↔{t}={A}{u}+{B}{v}\right)$
9 5 8 cbvrex2vw ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{t}={A}{x}+{B}{y}↔\exists {u}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}{t}={A}{u}+{B}{v}$
10 2 9 syl6bb ${⊢}{z}={t}\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}↔\exists {u}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}{t}={A}{u}+{B}{v}\right)$
11 10 cbvrabv ${⊢}\left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\}=\left\{{t}\in ℕ|\exists {u}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}{t}={A}{u}+{B}{v}\right\}$
12 simpll ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge ¬\left({A}=0\wedge {B}=0\right)\right)\to {A}\in ℤ$
13 simplr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge ¬\left({A}=0\wedge {B}=0\right)\right)\to {B}\in ℤ$
14 eqid ${⊢}sup\left(\left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\},ℝ,<\right)=sup\left(\left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\},ℝ,<\right)$
15 simpr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge ¬\left({A}=0\wedge {B}=0\right)\right)\to ¬\left({A}=0\wedge {B}=0\right)$
16 11 12 13 14 15 bezoutlem4 ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge ¬\left({A}=0\wedge {B}=0\right)\right)\to {A}\mathrm{gcd}{B}\in \left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\}$
17 eqeq1 ${⊢}{z}={A}\mathrm{gcd}{B}\to \left({z}={A}{x}+{B}{y}↔{A}\mathrm{gcd}{B}={A}{x}+{B}{y}\right)$
18 17 2rexbidv ${⊢}{z}={A}\mathrm{gcd}{B}\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}\right)$
19 18 elrab ${⊢}{A}\mathrm{gcd}{B}\in \left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\}↔\left({A}\mathrm{gcd}{B}\in ℕ\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}\right)$
20 19 simprbi ${⊢}{A}\mathrm{gcd}{B}\in \left\{{z}\in ℕ|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={A}{x}+{B}{y}\right\}\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}$
21 16 20 syl ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge ¬\left({A}=0\wedge {B}=0\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}$
22 21 ex ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(¬\left({A}=0\wedge {B}=0\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}\right)$
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\mathrm{gcd}0=0$
29 24 27 28 3eqtr4ri ${⊢}0\mathrm{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 \left(0\mathrm{gcd}0=0\cdot {x}+0\cdot {y}↔0\mathrm{gcd}0=0\cdot 0+0\cdot {y}\right)$
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 \left(0\mathrm{gcd}0=0\cdot 0+0\cdot {y}↔0\mathrm{gcd}0=0\cdot 0+0\cdot 0\right)$
36 32 35 rspc2ev ${⊢}\left(0\in ℤ\wedge 0\in ℤ\wedge 0\mathrm{gcd}0=0\cdot 0+0\cdot 0\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}0\mathrm{gcd}0=0\cdot {x}+0\cdot {y}$
37 23 23 29 36 mp3an ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}0\mathrm{gcd}0=0\cdot {x}+0\cdot {y}$
38 oveq12 ${⊢}\left({A}=0\wedge {B}=0\right)\to {A}\mathrm{gcd}{B}=0\mathrm{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 ${⊢}\left({A}=0\wedge {B}=0\right)\to {A}{x}+{B}{y}=0\cdot {x}+0\cdot {y}$
42 38 41 eqeq12d ${⊢}\left({A}=0\wedge {B}=0\right)\to \left({A}\mathrm{gcd}{B}={A}{x}+{B}{y}↔0\mathrm{gcd}0=0\cdot {x}+0\cdot {y}\right)$
43 42 2rexbidv ${⊢}\left({A}=0\wedge {B}=0\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}0\mathrm{gcd}0=0\cdot {x}+0\cdot {y}\right)$
44 37 43 mpbiri ${⊢}\left({A}=0\wedge {B}=0\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}$
45 22 44 pm2.61d2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{A}\mathrm{gcd}{B}={A}{x}+{B}{y}$