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