Metamath Proof Explorer

Theorem dvdsmulc

Description: Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

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