This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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