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 KMNK MNMN

Proof

Step Hyp Ref Expression
1 zmulcl KMK M
2 1 anim1i KMNK MN
3 2 3impa KMNK MN
4 3simpc KMNMN
5 zmulcl xKxK
6 5 ancoms KxxK
7 6 3ad2antl1 KMNxxK
8 zcn xx
9 zcn KK
10 zcn MM
11 mulass xKMxK M=xK M
12 8 9 10 11 syl3an xKMxK M=xK M
13 12 3coml KMxxK M=xK M
14 13 3expa KMxxK M=xK M
15 14 3adantl3 KMNxxK M=xK M
16 15 eqeq1d KMNxxK M=NxK M=N
17 16 biimprd KMNxxK M=NxK M=N
18 3 4 7 17 dvds1lem KMNK MNMN