Metamath Proof Explorer

Theorem dvdsmulcr

Description: Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdsmulcr 
|- ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M x. K ) || ( N x. K ) <-> M || N ) )

Proof

Step Hyp Ref Expression
1 zmulcl 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M x. K ) e. ZZ )
2 1 3adant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M x. K ) e. ZZ )
3 zmulcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N x. K ) e. ZZ )
4 3 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( N x. K ) e. ZZ )
5 2 4 jca 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( M x. K ) e. ZZ /\ ( N x. K ) e. ZZ ) )
6 5 3adant3r 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M x. K ) e. ZZ /\ ( N x. K ) e. ZZ ) )
7 3simpa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( M e. ZZ /\ N e. ZZ ) )
8 simpr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) /\ x e. ZZ ) -> x e. ZZ )
9 zcn 
 |-  ( x e. ZZ -> x e. CC )
10 zcn 
 |-  ( M e. ZZ -> M e. CC )
11 9 10 anim12i 
 |-  ( ( x e. ZZ /\ M e. ZZ ) -> ( x e. CC /\ M e. CC ) )
12 zcn 
 |-  ( N e. ZZ -> N e. CC )
13 zcn 
 |-  ( K e. ZZ -> K e. CC )
14 13 anim1i 
 |-  ( ( K e. ZZ /\ K =/= 0 ) -> ( K e. CC /\ K =/= 0 ) )
15 mulass 
 |-  ( ( x e. CC /\ M e. CC /\ K e. CC ) -> ( ( x x. M ) x. K ) = ( x x. ( M x. K ) ) )
16 15 3expa 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ K e. CC ) -> ( ( x x. M ) x. K ) = ( x x. ( M x. K ) ) )
17 16 adantrr 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( x x. M ) x. K ) = ( x x. ( M x. K ) ) )
18 17 3adant2 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ N e. CC /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( x x. M ) x. K ) = ( x x. ( M x. K ) ) )
19 18 eqeq1d 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ N e. CC /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( ( x x. M ) x. K ) = ( N x. K ) <-> ( x x. ( M x. K ) ) = ( N x. K ) ) )
20 mulcl 
 |-  ( ( x e. CC /\ M e. CC ) -> ( x x. M ) e. CC )
21 mulcan2 
 |-  ( ( ( x x. M ) e. CC /\ N e. CC /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( ( x x. M ) x. K ) = ( N x. K ) <-> ( x x. M ) = N ) )
22 20 21 syl3an1 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ N e. CC /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( ( x x. M ) x. K ) = ( N x. K ) <-> ( x x. M ) = N ) )
23 19 22 bitr3d 
 |-  ( ( ( x e. CC /\ M e. CC ) /\ N e. CC /\ ( K e. CC /\ K =/= 0 ) ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
24 11 12 14 23 syl3an 
 |-  ( ( ( x e. ZZ /\ M e. ZZ ) /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
25 24 3expb 
 |-  ( ( ( x e. ZZ /\ M e. ZZ ) /\ ( N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
26 25 3impa 
 |-  ( ( x e. ZZ /\ M e. ZZ /\ ( N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
27 26 3coml 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) /\ x e. ZZ ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
28 27 3expia 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) ) -> ( x e. ZZ -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) ) )
29 28 3impb 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( x e. ZZ -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) ) )
30 29 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) /\ x e. ZZ ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) <-> ( x x. M ) = N ) )
31 30 biimpd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) /\ x e. ZZ ) -> ( ( x x. ( M x. K ) ) = ( N x. K ) -> ( x x. M ) = N ) )
32 6 7 8 31 dvds1lem 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M x. K ) || ( N x. K ) -> M || N ) )
33 dvdsmulc 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M || N -> ( M x. K ) || ( N x. K ) ) )
34 33 3adant3r 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( M || N -> ( M x. K ) || ( N x. K ) ) )
35 32 34 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M x. K ) || ( N x. K ) <-> M || N ) )