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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gcdcl | |
|
2 | 1 | nn0zd | |
3 | 2 | adantr | |
4 | simpll | |
|
5 | simprl | |
|
6 | 4 5 | zmulcld | |
7 | simplr | |
|
8 | simprr | |
|
9 | 7 8 | zmulcld | |
10 | gcddvds | |
|
11 | 10 | adantr | |
12 | 11 | simpld | |
13 | 3 4 5 12 | dvdsmultr1d | |
14 | 11 | simprd | |
15 | 3 7 8 14 | dvdsmultr1d | |
16 | 3 6 9 13 15 | dvds2addd | |