# Metamath Proof Explorer

## Theorem dvds0lem

Description: A lemma to assist theorems of || with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds0lem ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\cdot {M}={N}\right)\to {M}\parallel {N}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{x}={K}\to {x}\cdot {M}={K}\cdot {M}$
2 1 eqeq1d ${⊢}{x}={K}\to \left({x}\cdot {M}={N}↔{K}\cdot {M}={N}\right)$
3 2 rspcev ${⊢}\left({K}\in ℤ\wedge {K}\cdot {M}={N}\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{x}\cdot {M}={N}$
4 3 adantl ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {K}\cdot {M}={N}\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{x}\cdot {M}={N}$
5 divides ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\parallel {N}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{x}\cdot {M}={N}\right)$
6 5 adantr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {K}\cdot {M}={N}\right)\right)\to \left({M}\parallel {N}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{x}\cdot {M}={N}\right)$
7 4 6 mpbird ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {K}\cdot {M}={N}\right)\right)\to {M}\parallel {N}$
8 7 expr ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)\to \left({K}\cdot {M}={N}\to {M}\parallel {N}\right)$
9 8 3impa ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\to \left({K}\cdot {M}={N}\to {M}\parallel {N}\right)$
10 9 3comr ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\cdot {M}={N}\to {M}\parallel {N}\right)$
11 10 imp ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\cdot {M}={N}\right)\to {M}\parallel {N}$