zdiv

Description: Two ways to express " M divides N ". (Contributed by NM, 3-Oct-2008)

		Ref	Expression
	Assertion	zdiv	$⊢ (M \in ℕ \land N \in ℤ) \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ)$

Proof

Step	Hyp	Ref	Expression
1		nnne0	$⊢ M \in ℕ \to M \neq 0$
2	1	adantr	$⊢ (M \in ℕ \land N \in ℤ) \to M \neq 0$
3		nncn	$⊢ M \in ℕ \to M \in ℂ$
4		zcn	$⊢ N \in ℤ \to N \in ℂ$
5		zcn	$⊢ k \in ℤ \to k \in ℂ$
6		divcan3	$⊢ (k \in ℂ \land M \in ℂ \land M \neq 0) \to \frac{M k}{M} = k$
7	6	3coml	$⊢ (M \in ℂ \land M \neq 0 \land k \in ℂ) \to \frac{M k}{M} = k$
8	7	3expa	$⊢ ((M \in ℂ \land M \neq 0) \land k \in ℂ) \to \frac{M k}{M} = k$
9	5 8	sylan2	$⊢ ((M \in ℂ \land M \neq 0) \land k \in ℤ) \to \frac{M k}{M} = k$
10	9	3adantl2	$⊢ ((M \in ℂ \land N \in ℂ \land M \neq 0) \land k \in ℤ) \to \frac{M k}{M} = k$
11		oveq1	$⊢ M k = N \to \frac{M k}{M} = \frac{N}{M}$
12	10 11	sylan9req	$⊢ (((M \in ℂ \land N \in ℂ \land M \neq 0) \land k \in ℤ) \land M k = N) \to k = \frac{N}{M}$
13		simplr	$⊢ (((M \in ℂ \land N \in ℂ \land M \neq 0) \land k \in ℤ) \land M k = N) \to k \in ℤ$
14	12 13	eqeltrrd	$⊢ (((M \in ℂ \land N \in ℂ \land M \neq 0) \land k \in ℤ) \land M k = N) \to \frac{N}{M} \in ℤ$
15	14	rexlimdva2	$⊢ (M \in ℂ \land N \in ℂ \land M \neq 0) \to (\exists k \in ℤ M k = N \to \frac{N}{M} \in ℤ)$
16		divcan2	$⊢ (N \in ℂ \land M \in ℂ \land M \neq 0) \to M (\frac{N}{M}) = N$
17	16	3com12	$⊢ (M \in ℂ \land N \in ℂ \land M \neq 0) \to M (\frac{N}{M}) = N$
18		oveq2	$⊢ k = \frac{N}{M} \to M k = M (\frac{N}{M})$
19	18	eqeq1d	$⊢ k = \frac{N}{M} \to (M k = N \leftrightarrow M (\frac{N}{M}) = N)$
20	19	rspcev	$⊢ (\frac{N}{M} \in ℤ \land M (\frac{N}{M}) = N) \to \exists k \in ℤ M k = N$
21	20	expcom	$⊢ M (\frac{N}{M}) = N \to (\frac{N}{M} \in ℤ \to \exists k \in ℤ M k = N)$
22	17 21	syl	$⊢ (M \in ℂ \land N \in ℂ \land M \neq 0) \to (\frac{N}{M} \in ℤ \to \exists k \in ℤ M k = N)$
23	15 22	impbid	$⊢ (M \in ℂ \land N \in ℂ \land M \neq 0) \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ)$
24	23	3expia	$⊢ (M \in ℂ \land N \in ℂ) \to (M \neq 0 \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ))$
25	3 4 24	syl2an	$⊢ (M \in ℕ \land N \in ℤ) \to (M \neq 0 \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ))$
26	2 25	mpd	$⊢ (M \in ℕ \land N \in ℤ) \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ)$

Metamath Proof Explorer

Theorem zdiv

Proof