Metamath Proof Explorer

Theorem dvdscmul

Description: Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in ApostolNT p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdscmul 
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M || N -> ( K x. M ) || ( K x. N ) ) )

Proof

Step Hyp Ref Expression
1 3simpc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
2 zmulcl 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. ZZ )
3 2 3adant3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K x. M ) e. ZZ )
4 zmulcl 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )
5 4 3adant2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K x. N ) e. ZZ )
6 3 5 jca 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) e. ZZ /\ ( K x. N ) e. ZZ ) )
7 simpr 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> x e. ZZ )
8 zcn 
 |-  ( x e. ZZ -> x e. CC )
9 zcn 
 |-  ( K e. ZZ -> K e. CC )
10 zcn 
 |-  ( M e. ZZ -> M e. CC )
11 mul12 
 |-  ( ( x e. CC /\ K e. CC /\ M e. CC ) -> ( x x. ( K x. M ) ) = ( K x. ( x x. M ) ) )
12 8 9 10 11 syl3an 
 |-  ( ( x e. ZZ /\ K e. ZZ /\ M e. ZZ ) -> ( x x. ( K x. M ) ) = ( K x. ( x x. M ) ) )
13 12 3coml 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( K x. ( x x. M ) ) )
14 13 3expa 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( K x. ( x x. M ) ) )
15 14 3adantl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( K x. ( x x. M ) ) )
16 oveq2 
 |-  ( ( x x. M ) = N -> ( K x. ( x x. M ) ) = ( K x. N ) )
17 15 16 sylan9eq 
 |-  ( ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) /\ ( x x. M ) = N ) -> ( x x. ( K x. M ) ) = ( K x. N ) )
18 17 ex 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. M ) = N -> ( x x. ( K x. M ) ) = ( K x. N ) ) )
19 1 6 7 18 dvds1lem 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M || N -> ( K x. M ) || ( K x. N ) ) )
20 19 3coml 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M || N -> ( K x. M ) || ( K x. N ) ) )