Metamath Proof Explorer


Theorem bezoutr

Description: Partial converse to bezout . Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion bezoutr
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. NN0 )
2 1 nn0zd
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) e. ZZ )
3 2 adantr
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) e. ZZ )
4 simpll
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> A e. ZZ )
5 simprl
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> X e. ZZ )
6 4 5 zmulcld
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A x. X ) e. ZZ )
7 simplr
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> B e. ZZ )
8 simprr
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> Y e. ZZ )
9 7 8 zmulcld
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( B x. Y ) e. ZZ )
10 gcddvds
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
11 10 adantr
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
12 11 simpld
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || A )
13 3 4 5 12 dvdsmultr1d
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( A x. X ) )
14 11 simprd
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || B )
15 3 7 8 14 dvdsmultr1d
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( B x. Y ) )
16 dvds2add
 |-  ( ( ( A gcd B ) e. ZZ /\ ( A x. X ) e. ZZ /\ ( B x. Y ) e. ZZ ) -> ( ( ( A gcd B ) || ( A x. X ) /\ ( A gcd B ) || ( B x. Y ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) ) )
17 16 imp
 |-  ( ( ( ( A gcd B ) e. ZZ /\ ( A x. X ) e. ZZ /\ ( B x. Y ) e. ZZ ) /\ ( ( A gcd B ) || ( A x. X ) /\ ( A gcd B ) || ( B x. Y ) ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) )
18 3 6 9 13 15 17 syl32anc
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) )