Metamath Proof Explorer


Theorem dvdsmulgcd

Description: A divisibility equivalent for odmulg . (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion dvdsmulgcd BCABCABCgcdA

Proof

Step Hyp Ref Expression
1 simplr BCABCC
2 dvdszrcl ABCABC
3 2 adantl BCABCABC
4 3 simpld BCABCA
5 bezout CAxyCgcdA=Cx+Ay
6 1 4 5 syl2anc BCABCxyCgcdA=Cx+Ay
7 4 adantr BCABCxyA
8 simplll BCABCxyB
9 simpllr BCABCxyC
10 simprl BCABCxyx
11 9 10 zmulcld BCABCxyCx
12 8 11 zmulcld BCABCxyBCx
13 simprr BCABCxyy
14 7 13 zmulcld BCABCxyAy
15 8 14 zmulcld BCABCxyBAy
16 8 9 zmulcld BCABCxyBC
17 simplr BCABCxyABC
18 7 16 10 17 dvdsmultr1d BCABCxyABCx
19 8 zcnd BCABCxyB
20 9 zcnd BCABCxyC
21 10 zcnd BCABCxyx
22 19 20 21 mulassd BCABCxyBCx=BCx
23 18 22 breqtrd BCABCxyABCx
24 8 13 zmulcld BCABCxyBy
25 dvdsmul1 AByAABy
26 7 24 25 syl2anc BCABCxyAABy
27 7 zcnd BCABCxyA
28 13 zcnd BCABCxyy
29 19 27 28 mul12d BCABCxyBAy=ABy
30 26 29 breqtrrd BCABCxyABAy
31 7 12 15 23 30 dvds2addd BCABCxyABCx+BAy
32 11 zcnd BCABCxyCx
33 14 zcnd BCABCxyAy
34 19 32 33 adddid BCABCxyBCx+Ay=BCx+BAy
35 31 34 breqtrrd BCABCxyABCx+Ay
36 oveq2 CgcdA=Cx+AyBCgcdA=BCx+Ay
37 36 breq2d CgcdA=Cx+AyABCgcdAABCx+Ay
38 35 37 syl5ibrcom BCABCxyCgcdA=Cx+AyABCgcdA
39 38 rexlimdvva BCABCxyCgcdA=Cx+AyABCgcdA
40 6 39 mpd BCABCABCgcdA
41 dvdszrcl ABCgcdAABCgcdA
42 41 adantl BCABCgcdAABCgcdA
43 42 simpld BCABCgcdAA
44 42 simprd BCABCgcdABCgcdA
45 zmulcl BCBC
46 45 adantr BCABCgcdABC
47 simpr BCABCgcdAABCgcdA
48 simplr BCABCgcdAC
49 gcddvds CACgcdACCgcdAA
50 48 43 49 syl2anc BCABCgcdACgcdACCgcdAA
51 50 simpld BCABCgcdACgcdAC
52 48 43 gcdcld BCABCgcdACgcdA0
53 52 nn0zd BCABCgcdACgcdA
54 simpll BCABCgcdAB
55 dvdscmul CgcdACBCgcdACBCgcdABC
56 53 48 54 55 syl3anc BCABCgcdACgcdACBCgcdABC
57 51 56 mpd BCABCgcdABCgcdABC
58 43 44 46 47 57 dvdstrd BCABCgcdAABC
59 40 58 impbida BCABCABCgcdA