Description: If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | muldvds2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zmulcl | |
|
2 | 1 | anim1i | |
3 | 2 | 3impa | |
4 | 3simpc | |
|
5 | zmulcl | |
|
6 | 5 | ancoms | |
7 | 6 | 3ad2antl1 | |
8 | zcn | |
|
9 | zcn | |
|
10 | zcn | |
|
11 | mulass | |
|
12 | 8 9 10 11 | syl3an | |
13 | 12 | 3coml | |
14 | 13 | 3expa | |
15 | 14 | 3adantl3 | |
16 | 15 | eqeq1d | |
17 | 16 | biimprd | |
18 | 3 4 7 17 | dvds1lem | |