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 ABXYAgcdBAX+BY

Proof

Step Hyp Ref Expression
1 gcdcl ABAgcdB0
2 1 nn0zd ABAgcdB
3 2 adantr ABXYAgcdB
4 simpll ABXYA
5 simprl ABXYX
6 4 5 zmulcld ABXYAX
7 simplr ABXYB
8 simprr ABXYY
9 7 8 zmulcld ABXYBY
10 gcddvds ABAgcdBAAgcdBB
11 10 adantr ABXYAgcdBAAgcdBB
12 11 simpld ABXYAgcdBA
13 3 4 5 12 dvdsmultr1d ABXYAgcdBAX
14 11 simprd ABXYAgcdBB
15 3 7 8 14 dvdsmultr1d ABXYAgcdBBY
16 3 6 9 13 15 dvds2addd ABXYAgcdBAX+BY