Metamath Proof Explorer

Theorem muldvds1

Description: If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 zmulcl 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. ZZ )
2 1 anim1i 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) -> ( ( K x. M ) e. ZZ /\ N e. ZZ ) )
3 2 3impa 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) e. ZZ /\ N e. ZZ ) )
4 3simpb 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ZZ /\ N e. ZZ ) )
5 zmulcl 
 |-  ( ( x e. ZZ /\ M e. ZZ ) -> ( x x. M ) e. ZZ )
6 5 ancoms 
 |-  ( ( M e. ZZ /\ x e. ZZ ) -> ( x x. M ) e. ZZ )
7 6 3ad2antl2 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( x x. M ) 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 mulass 
 |-  ( ( x e. CC /\ K e. CC /\ M e. CC ) -> ( ( x x. K ) x. M ) = ( x x. ( K x. M ) ) )
12 mul32 
 |-  ( ( x e. CC /\ K e. CC /\ M e. CC ) -> ( ( x x. K ) x. M ) = ( ( x x. M ) x. K ) )
13 11 12 eqtr3d 
 |-  ( ( x e. CC /\ K e. CC /\ M e. CC ) -> ( x x. ( K x. M ) ) = ( ( x x. M ) x. K ) )
14 8 9 10 13 syl3an 
 |-  ( ( x e. ZZ /\ K e. ZZ /\ M e. ZZ ) -> ( x x. ( K x. M ) ) = ( ( x x. M ) x. K ) )
15 14 3coml 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( ( x x. M ) x. K ) )
16 15 3expa 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( ( x x. M ) x. K ) )
17 16 3adantl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( x x. ( K x. M ) ) = ( ( x x. M ) x. K ) )
18 17 eqeq1d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. ( K x. M ) ) = N <-> ( ( x x. M ) x. K ) = N ) )
19 18 biimpd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. ( K x. M ) ) = N -> ( ( x x. M ) x. K ) = N ) )
20 3 4 7 19 dvds1lem 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> K || N ) )