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