# Metamath Proof Explorer

## Theorem dvdsval2

Description: One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion dvdsval2 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left({M}\parallel {N}↔\frac{{N}}{{M}}\in ℤ\right)$

### Proof

Step Hyp Ref Expression
1 divides ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\parallel {N}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}\right)$
2 1 3adant2 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left({M}\parallel {N}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}\right)$
3 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
4 3 3ad2ant3 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to {N}\in ℂ$
5 4 adantr ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to {N}\in ℂ$
6 zcn ${⊢}{k}\in ℤ\to {k}\in ℂ$
7 6 adantl ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to {k}\in ℂ$
8 zcn ${⊢}{M}\in ℤ\to {M}\in ℂ$
9 8 3ad2ant1 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to {M}\in ℂ$
10 9 adantr ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to {M}\in ℂ$
11 simpl2 ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to {M}\ne 0$
12 5 7 10 11 divmul3d ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to \left(\frac{{N}}{{M}}={k}↔{N}={k}\cdot {M}\right)$
13 eqcom ${⊢}{N}={k}\cdot {M}↔{k}\cdot {M}={N}$
14 12 13 syl6bb ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to \left(\frac{{N}}{{M}}={k}↔{k}\cdot {M}={N}\right)$
15 14 biimprd ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge {k}\in ℤ\right)\to \left({k}\cdot {M}={N}\to \frac{{N}}{{M}}={k}\right)$
16 15 impr ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \left({k}\in ℤ\wedge {k}\cdot {M}={N}\right)\right)\to \frac{{N}}{{M}}={k}$
17 simprl ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \left({k}\in ℤ\wedge {k}\cdot {M}={N}\right)\right)\to {k}\in ℤ$
18 16 17 eqeltrd ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \left({k}\in ℤ\wedge {k}\cdot {M}={N}\right)\right)\to \frac{{N}}{{M}}\in ℤ$
19 18 rexlimdvaa ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}\to \frac{{N}}{{M}}\in ℤ\right)$
20 simpr ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \frac{{N}}{{M}}\in ℤ\right)\to \frac{{N}}{{M}}\in ℤ$
21 simp2 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to {M}\ne 0$
22 4 9 21 divcan1d ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left(\frac{{N}}{{M}}\right)\cdot {M}={N}$
23 22 adantr ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \frac{{N}}{{M}}\in ℤ\right)\to \left(\frac{{N}}{{M}}\right)\cdot {M}={N}$
24 oveq1 ${⊢}{k}=\frac{{N}}{{M}}\to {k}\cdot {M}=\left(\frac{{N}}{{M}}\right)\cdot {M}$
25 24 eqeq1d ${⊢}{k}=\frac{{N}}{{M}}\to \left({k}\cdot {M}={N}↔\left(\frac{{N}}{{M}}\right)\cdot {M}={N}\right)$
26 25 rspcev ${⊢}\left(\frac{{N}}{{M}}\in ℤ\wedge \left(\frac{{N}}{{M}}\right)\cdot {M}={N}\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}$
27 20 23 26 syl2anc ${⊢}\left(\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\wedge \frac{{N}}{{M}}\in ℤ\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}$
28 27 ex ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left(\frac{{N}}{{M}}\in ℤ\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}\right)$
29 19 28 impbid ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{k}\cdot {M}={N}↔\frac{{N}}{{M}}\in ℤ\right)$
30 2 29 bitrd ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {N}\in ℤ\right)\to \left({M}\parallel {N}↔\frac{{N}}{{M}}\in ℤ\right)$