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	$⊢ (M \in ℤ \land M \neq 0 \land N \in ℤ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$

Proof

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

Metamath Proof Explorer

Theorem dvdsval2

Proof