Metamath Proof Explorer

Theorem dvdscmulr

Description: Cancellation law for the divides relation. Theorem 1.1(e) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

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