Description: A divisibility equivalent for odmulg . (Contributed by Stefan O'Rear, 6-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsmulgcd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr | |
|
2 | dvdszrcl | |
|
3 | 2 | adantl | |
4 | 3 | simpld | |
5 | bezout | |
|
6 | 1 4 5 | syl2anc | |
7 | 4 | adantr | |
8 | simplll | |
|
9 | simpllr | |
|
10 | simprl | |
|
11 | 9 10 | zmulcld | |
12 | 8 11 | zmulcld | |
13 | simprr | |
|
14 | 7 13 | zmulcld | |
15 | 8 14 | zmulcld | |
16 | 8 9 | zmulcld | |
17 | simplr | |
|
18 | 7 16 10 17 | dvdsmultr1d | |
19 | 8 | zcnd | |
20 | 9 | zcnd | |
21 | 10 | zcnd | |
22 | 19 20 21 | mulassd | |
23 | 18 22 | breqtrd | |
24 | 8 13 | zmulcld | |
25 | dvdsmul1 | |
|
26 | 7 24 25 | syl2anc | |
27 | 7 | zcnd | |
28 | 13 | zcnd | |
29 | 19 27 28 | mul12d | |
30 | 26 29 | breqtrrd | |
31 | 7 12 15 23 30 | dvds2addd | |
32 | 11 | zcnd | |
33 | 14 | zcnd | |
34 | 19 32 33 | adddid | |
35 | 31 34 | breqtrrd | |
36 | oveq2 | |
|
37 | 36 | breq2d | |
38 | 35 37 | syl5ibrcom | |
39 | 38 | rexlimdvva | |
40 | 6 39 | mpd | |
41 | dvdszrcl | |
|
42 | 41 | adantl | |
43 | 42 | simpld | |
44 | 42 | simprd | |
45 | zmulcl | |
|
46 | 45 | adantr | |
47 | simpr | |
|
48 | simplr | |
|
49 | gcddvds | |
|
50 | 48 43 49 | syl2anc | |
51 | 50 | simpld | |
52 | 48 43 | gcdcld | |
53 | 52 | nn0zd | |
54 | simpll | |
|
55 | dvdscmul | |
|
56 | 53 48 54 55 | syl3anc | |
57 | 51 56 | mpd | |
58 | 43 44 46 47 57 | dvdstrd | |
59 | 40 58 | impbida | |