Metamath Proof Explorer


Theorem dvdsmulgcd

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

Ref Expression
Assertion dvdsmulgcd
|- ( ( B e. ZZ /\ C e. ZZ ) -> ( A || ( B x. C ) <-> A || ( B x. ( C gcd A ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> C e. ZZ )
2 dvdszrcl
 |-  ( A || ( B x. C ) -> ( A e. ZZ /\ ( B x. C ) e. ZZ ) )
3 2 adantl
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> ( A e. ZZ /\ ( B x. C ) e. ZZ ) )
4 3 simpld
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> A e. ZZ )
5 bezout
 |-  ( ( C e. ZZ /\ A e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) )
6 1 4 5 syl2anc
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> E. x e. ZZ E. y e. ZZ ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) )
7 4 adantr
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A e. ZZ )
8 simplll
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> B e. ZZ )
9 simpllr
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> C e. ZZ )
10 simprl
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
11 9 10 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( C x. x ) e. ZZ )
12 8 11 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. ( C x. x ) ) e. ZZ )
13 simprr
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
14 7 13 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( A x. y ) e. ZZ )
15 8 14 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. ( A x. y ) ) e. ZZ )
16 8 9 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. C ) e. ZZ )
17 simplr
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( B x. C ) )
18 7 16 10 17 dvdsmultr1d
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( ( B x. C ) x. x ) )
19 8 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> B e. CC )
20 9 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> C e. CC )
21 10 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. CC )
22 19 20 21 mulassd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( B x. C ) x. x ) = ( B x. ( C x. x ) ) )
23 18 22 breqtrd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( B x. ( C x. x ) ) )
24 8 13 zmulcld
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. y ) e. ZZ )
25 dvdsmul1
 |-  ( ( A e. ZZ /\ ( B x. y ) e. ZZ ) -> A || ( A x. ( B x. y ) ) )
26 7 24 25 syl2anc
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( A x. ( B x. y ) ) )
27 7 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A e. CC )
28 13 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. CC )
29 19 27 28 mul12d
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. ( A x. y ) ) = ( A x. ( B x. y ) ) )
30 26 29 breqtrrd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( B x. ( A x. y ) ) )
31 dvds2add
 |-  ( ( A e. ZZ /\ ( B x. ( C x. x ) ) e. ZZ /\ ( B x. ( A x. y ) ) e. ZZ ) -> ( ( A || ( B x. ( C x. x ) ) /\ A || ( B x. ( A x. y ) ) ) -> A || ( ( B x. ( C x. x ) ) + ( B x. ( A x. y ) ) ) ) )
32 31 imp
 |-  ( ( ( A e. ZZ /\ ( B x. ( C x. x ) ) e. ZZ /\ ( B x. ( A x. y ) ) e. ZZ ) /\ ( A || ( B x. ( C x. x ) ) /\ A || ( B x. ( A x. y ) ) ) ) -> A || ( ( B x. ( C x. x ) ) + ( B x. ( A x. y ) ) ) )
33 7 12 15 23 30 32 syl32anc
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( ( B x. ( C x. x ) ) + ( B x. ( A x. y ) ) ) )
34 11 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( C x. x ) e. CC )
35 14 zcnd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( A x. y ) e. CC )
36 19 34 35 adddid
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( B x. ( ( C x. x ) + ( A x. y ) ) ) = ( ( B x. ( C x. x ) ) + ( B x. ( A x. y ) ) ) )
37 33 36 breqtrrd
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A || ( B x. ( ( C x. x ) + ( A x. y ) ) ) )
38 oveq2
 |-  ( ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) -> ( B x. ( C gcd A ) ) = ( B x. ( ( C x. x ) + ( A x. y ) ) ) )
39 38 breq2d
 |-  ( ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) -> ( A || ( B x. ( C gcd A ) ) <-> A || ( B x. ( ( C x. x ) + ( A x. y ) ) ) ) )
40 37 39 syl5ibrcom
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) -> A || ( B x. ( C gcd A ) ) ) )
41 40 rexlimdvva
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> ( E. x e. ZZ E. y e. ZZ ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) -> A || ( B x. ( C gcd A ) ) ) )
42 6 41 mpd
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> A || ( B x. ( C gcd A ) ) )
43 dvdszrcl
 |-  ( A || ( B x. ( C gcd A ) ) -> ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ ) )
44 43 adantl
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ ) )
45 44 simpld
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A e. ZZ )
46 44 simprd
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. ( C gcd A ) ) e. ZZ )
47 zmulcl
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. ZZ )
48 47 adantr
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. C ) e. ZZ )
49 simpr
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A || ( B x. ( C gcd A ) ) )
50 simplr
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> C e. ZZ )
51 gcddvds
 |-  ( ( C e. ZZ /\ A e. ZZ ) -> ( ( C gcd A ) || C /\ ( C gcd A ) || A ) )
52 50 45 51 syl2anc
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( ( C gcd A ) || C /\ ( C gcd A ) || A ) )
53 52 simpld
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) || C )
54 50 45 gcdcld
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) e. NN0 )
55 54 nn0zd
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) e. ZZ )
56 simpll
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> B e. ZZ )
57 dvdscmul
 |-  ( ( ( C gcd A ) e. ZZ /\ C e. ZZ /\ B e. ZZ ) -> ( ( C gcd A ) || C -> ( B x. ( C gcd A ) ) || ( B x. C ) ) )
58 55 50 56 57 syl3anc
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( ( C gcd A ) || C -> ( B x. ( C gcd A ) ) || ( B x. C ) ) )
59 53 58 mpd
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. ( C gcd A ) ) || ( B x. C ) )
60 dvdstr
 |-  ( ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ /\ ( B x. C ) e. ZZ ) -> ( ( A || ( B x. ( C gcd A ) ) /\ ( B x. ( C gcd A ) ) || ( B x. C ) ) -> A || ( B x. C ) ) )
61 60 imp
 |-  ( ( ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ /\ ( B x. C ) e. ZZ ) /\ ( A || ( B x. ( C gcd A ) ) /\ ( B x. ( C gcd A ) ) || ( B x. C ) ) ) -> A || ( B x. C ) )
62 45 46 48 49 59 61 syl32anc
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A || ( B x. C ) )
63 42 62 impbida
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( A || ( B x. C ) <-> A || ( B x. ( C gcd A ) ) ) )