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 e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = 1 -> ( A gcd B ) = 1 ) )

Proof

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