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