Metamath Proof Explorer

Theorem muldvds2

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

Ref Expression
Assertion muldvds2 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> M || 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 3simpc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
5 zmulcl 
 |-  ( ( x e. ZZ /\ K e. ZZ ) -> ( x x. K ) e. ZZ )
6 5 ancoms 
 |-  ( ( K e. ZZ /\ x e. ZZ ) -> ( x x. K ) e. ZZ )
7 6 3ad2antl1 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( x x. K ) 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 8 9 10 11 syl3an 
 |-  ( ( x e. ZZ /\ K e. ZZ /\ M e. ZZ ) -> ( ( x x. K ) x. M ) = ( x x. ( K x. M ) ) )
13 12 3coml 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ x e. ZZ ) -> ( ( x x. K ) x. M ) = ( x x. ( K x. M ) ) )
14 13 3expa 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ x e. ZZ ) -> ( ( x x. K ) x. M ) = ( x x. ( K x. M ) ) )
15 14 3adantl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. K ) x. M ) = ( x x. ( K x. M ) ) )
16 15 eqeq1d 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( ( x x. K ) x. M ) = N <-> ( x x. ( K x. M ) ) = N ) )
17 16 biimprd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ x e. ZZ ) -> ( ( x x. ( K x. M ) ) = N -> ( ( x x. K ) x. M ) = N ) )
18 3 4 7 17 dvds1lem 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> M || N ) )