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 7 12 15 23 30 dvds2addd 
 |-  ( ( ( ( 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 ) ) ) )
32 11 zcnd 
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( C x. x ) e. CC )
33 14 zcnd 
 |-  ( ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( A x. y ) e. CC )
34 19 32 33 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 ) ) ) )
35 31 34 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 ) ) ) )
36 oveq2 
 |-  ( ( C gcd A ) = ( ( C x. x ) + ( A x. y ) ) -> ( B x. ( C gcd A ) ) = ( B x. ( ( C x. x ) + ( A x. y ) ) ) )
37 36 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 ) ) ) ) )
38 35 37 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 ) ) ) )
39 38 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 ) ) ) )
40 6 39 mpd 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. C ) ) -> A || ( B x. ( C gcd A ) ) )
41 dvdszrcl 
 |-  ( A || ( B x. ( C gcd A ) ) -> ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ ) )
42 41 adantl 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( A e. ZZ /\ ( B x. ( C gcd A ) ) e. ZZ ) )
43 42 simpld 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A e. ZZ )
44 42 simprd 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. ( C gcd A ) ) e. ZZ )
45 zmulcl 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. ZZ )
46 45 adantr 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. C ) e. ZZ )
47 simpr 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A || ( B x. ( C gcd A ) ) )
48 simplr 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> C e. ZZ )
49 gcddvds 
 |-  ( ( C e. ZZ /\ A e. ZZ ) -> ( ( C gcd A ) || C /\ ( C gcd A ) || A ) )
50 48 43 49 syl2anc 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( ( C gcd A ) || C /\ ( C gcd A ) || A ) )
51 50 simpld 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) || C )
52 48 43 gcdcld 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) e. NN0 )
53 52 nn0zd 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( C gcd A ) e. ZZ )
54 simpll 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> B e. ZZ )
55 dvdscmul 
 |-  ( ( ( C gcd A ) e. ZZ /\ C e. ZZ /\ B e. ZZ ) -> ( ( C gcd A ) || C -> ( B x. ( C gcd A ) ) || ( B x. C ) ) )
56 53 48 54 55 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 ) ) )
57 51 56 mpd 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> ( B x. ( C gcd A ) ) || ( B x. C ) )
58 43 44 46 47 57 dvdstrd 
 |-  ( ( ( B e. ZZ /\ C e. ZZ ) /\ A || ( B x. ( C gcd A ) ) ) -> A || ( B x. C ) )
59 40 58 impbida 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( A || ( B x. C ) <-> A || ( B x. ( C gcd A ) ) ) )