Metamath Proof Explorer


Theorem bezoutr1

Description: Converse of bezout for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion bezoutr1 A B X Y A X + B Y = 1 A gcd B = 1

Proof

Step Hyp Ref Expression
1 bezoutr A B X Y A gcd B A X + B Y
2 1 adantr A B X Y A X + B Y = 1 A gcd B A X + B Y
3 simpr A B X Y A X + B Y = 1 A X + B Y = 1
4 2 3 breqtrd A B X Y A X + B Y = 1 A gcd B 1
5 gcdcl A B A gcd B 0
6 5 nn0zd A B A gcd B
7 6 ad2antrr A B X Y A X + B Y = 1 A gcd B
8 1nn 1
9 8 a1i A B X Y A X + B Y = 1 1
10 dvdsle A gcd B 1 A gcd B 1 A gcd B 1
11 7 9 10 syl2anc A B X Y A X + B Y = 1 A gcd B 1 A gcd B 1
12 4 11 mpd A B X Y A X + B Y = 1 A gcd B 1
13 simpll A B X Y A X + B Y = 1 A B
14 oveq1 A = 0 A X = 0 X
15 oveq1 B = 0 B Y = 0 Y
16 14 15 oveqan12d A = 0 B = 0 A X + B Y = 0 X + 0 Y
17 zcn X X
18 17 mul02d X 0 X = 0
19 zcn Y Y
20 19 mul02d Y 0 Y = 0
21 18 20 oveqan12d X Y 0 X + 0 Y = 0 + 0
22 16 21 sylan9eqr X Y A = 0 B = 0 A X + B Y = 0 + 0
23 00id 0 + 0 = 0
24 22 23 eqtrdi X Y A = 0 B = 0 A X + B Y = 0
25 24 adantll A B X Y A = 0 B = 0 A X + B Y = 0
26 0ne1 0 1
27 26 a1i A B X Y A = 0 B = 0 0 1
28 25 27 eqnetrd A B X Y A = 0 B = 0 A X + B Y 1
29 28 ex A B X Y A = 0 B = 0 A X + B Y 1
30 29 necon2bd A B X Y A X + B Y = 1 ¬ A = 0 B = 0
31 30 imp A B X Y A X + B Y = 1 ¬ A = 0 B = 0
32 gcdn0cl A B ¬ A = 0 B = 0 A gcd B
33 13 31 32 syl2anc A B X Y A X + B Y = 1 A gcd B
34 nnle1eq1 A gcd B A gcd B 1 A gcd B = 1
35 33 34 syl A B X Y A X + B Y = 1 A gcd B 1 A gcd B = 1
36 12 35 mpbid A B X Y A X + B Y = 1 A gcd B = 1
37 36 ex A B X Y A X + B Y = 1 A gcd B = 1