# 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
`|- ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )`

### Proof

Step Hyp Ref Expression
1 eqeq1
` |-  ( z = t -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> t = ( ( A x. x ) + ( B x. y ) ) ) )`
2 1 2rexbidv
` |-  ( z = t -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ t = ( ( A x. x ) + ( B x. y ) ) ) )`
3 oveq2
` |-  ( x = u -> ( A x. x ) = ( A x. u ) )`
4 3 oveq1d
` |-  ( x = u -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. u ) + ( B x. y ) ) )`
5 4 eqeq2d
` |-  ( x = u -> ( t = ( ( A x. x ) + ( B x. y ) ) <-> t = ( ( A x. u ) + ( B x. y ) ) ) )`
6 oveq2
` |-  ( y = v -> ( B x. y ) = ( B x. v ) )`
7 6 oveq2d
` |-  ( y = v -> ( ( A x. u ) + ( B x. y ) ) = ( ( A x. u ) + ( B x. v ) ) )`
8 7 eqeq2d
` |-  ( y = v -> ( t = ( ( A x. u ) + ( B x. y ) ) <-> t = ( ( A x. u ) + ( B x. v ) ) ) )`
9 5 8 cbvrex2vw
` |-  ( E. x e. ZZ E. y e. ZZ t = ( ( A x. x ) + ( B x. y ) ) <-> E. u e. ZZ E. v e. ZZ t = ( ( A x. u ) + ( B x. v ) ) )`
10 2 9 syl6bb
` |-  ( z = t -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. u e. ZZ E. v e. ZZ t = ( ( A x. u ) + ( B x. v ) ) ) )`
11 10 cbvrabv
` |-  { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } = { t e. NN | E. u e. ZZ E. v e. ZZ t = ( ( A x. u ) + ( B x. v ) ) }`
12 simpll
` |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> A e. ZZ )`
13 simplr
` |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> B e. ZZ )`
14 eqid
` |-  inf ( { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } , RR , < ) = inf ( { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } , RR , < )`
15 simpr
` |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> -. ( A = 0 /\ B = 0 ) )`
16 11 12 13 14 15 bezoutlem4
` |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( A gcd B ) e. { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } )`
17 eqeq1
` |-  ( z = ( A gcd B ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) ) )`
18 17 2rexbidv
` |-  ( z = ( A gcd B ) -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) ) )`
19 18 elrab
` |-  ( ( A gcd B ) e. { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } <-> ( ( A gcd B ) e. NN /\ E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) ) )`
20 19 simprbi
` |-  ( ( A gcd B ) e. { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) } -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )`
21 16 20 syl
` |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )`
22 21 ex
` |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( -. ( A = 0 /\ B = 0 ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) ) )`
23 0z
` |-  0 e. ZZ`
24 00id
` |-  ( 0 + 0 ) = 0`
25 0cn
` |-  0 e. CC`
26 25 mul01i
` |-  ( 0 x. 0 ) = 0`
27 26 26 oveq12i
` |-  ( ( 0 x. 0 ) + ( 0 x. 0 ) ) = ( 0 + 0 )`
28 gcd0val
` |-  ( 0 gcd 0 ) = 0`
29 24 27 28 3eqtr4ri
` |-  ( 0 gcd 0 ) = ( ( 0 x. 0 ) + ( 0 x. 0 ) )`
30 oveq2
` |-  ( x = 0 -> ( 0 x. x ) = ( 0 x. 0 ) )`
31 30 oveq1d
` |-  ( x = 0 -> ( ( 0 x. x ) + ( 0 x. y ) ) = ( ( 0 x. 0 ) + ( 0 x. y ) ) )`
32 31 eqeq2d
` |-  ( x = 0 -> ( ( 0 gcd 0 ) = ( ( 0 x. x ) + ( 0 x. y ) ) <-> ( 0 gcd 0 ) = ( ( 0 x. 0 ) + ( 0 x. y ) ) ) )`
33 oveq2
` |-  ( y = 0 -> ( 0 x. y ) = ( 0 x. 0 ) )`
34 33 oveq2d
` |-  ( y = 0 -> ( ( 0 x. 0 ) + ( 0 x. y ) ) = ( ( 0 x. 0 ) + ( 0 x. 0 ) ) )`
35 34 eqeq2d
` |-  ( y = 0 -> ( ( 0 gcd 0 ) = ( ( 0 x. 0 ) + ( 0 x. y ) ) <-> ( 0 gcd 0 ) = ( ( 0 x. 0 ) + ( 0 x. 0 ) ) ) )`
36 32 35 rspc2ev
` |-  ( ( 0 e. ZZ /\ 0 e. ZZ /\ ( 0 gcd 0 ) = ( ( 0 x. 0 ) + ( 0 x. 0 ) ) ) -> E. x e. ZZ E. y e. ZZ ( 0 gcd 0 ) = ( ( 0 x. x ) + ( 0 x. y ) ) )`
37 23 23 29 36 mp3an
` |-  E. x e. ZZ E. y e. ZZ ( 0 gcd 0 ) = ( ( 0 x. x ) + ( 0 x. y ) )`
38 oveq12
` |-  ( ( A = 0 /\ B = 0 ) -> ( A gcd B ) = ( 0 gcd 0 ) )`
39 oveq1
` |-  ( A = 0 -> ( A x. x ) = ( 0 x. x ) )`
40 oveq1
` |-  ( B = 0 -> ( B x. y ) = ( 0 x. y ) )`
41 39 40 oveqan12d
` |-  ( ( A = 0 /\ B = 0 ) -> ( ( A x. x ) + ( B x. y ) ) = ( ( 0 x. x ) + ( 0 x. y ) ) )`
42 38 41 eqeq12d
` |-  ( ( A = 0 /\ B = 0 ) -> ( ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) <-> ( 0 gcd 0 ) = ( ( 0 x. x ) + ( 0 x. y ) ) ) )`
43 42 2rexbidv
` |-  ( ( A = 0 /\ B = 0 ) -> ( E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( 0 gcd 0 ) = ( ( 0 x. x ) + ( 0 x. y ) ) ) )`
44 37 43 mpbiri
` |-  ( ( A = 0 /\ B = 0 ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )`
45 22 44 pm2.61d2
` |-  ( ( A e. ZZ /\ B e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )`