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 B x y A gcd B = A x + B y

Proof

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