Metamath Proof Explorer

Theorem dvdsval3

Description: One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in ApostolNT p. 106. (Contributed by Mario Carneiro, 22-Feb-2014) (Revised by Mario Carneiro, 15-Jul-2014)

		Ref	Expression
	Assertion	dvdsval3	$⊢ (M \in ℕ \land N \in ℤ) \to (M ∥ N \leftrightarrow N \mod M = 0)$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ M \in ℕ \to M \in ℤ$
2		nnne0	$⊢ M \in ℕ \to M \neq 0$
3	1 2	jca	$⊢ M \in ℕ \to (M \in ℤ \land M \neq 0)$
4		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land N \in ℤ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$
5	4	3expa	$⊢ ((M \in ℤ \land M \neq 0) \land N \in ℤ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$
6	3 5	sylan	$⊢ (M \in ℕ \land N \in ℤ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$
7		zre	$⊢ N \in ℤ \to N \in ℝ$
8		nnrp	$⊢ M \in ℕ \to M \in ℝ^{+}$
9		mod0	$⊢ (N \in ℝ \land M \in ℝ^{+}) \to (N \mod M = 0 \leftrightarrow \frac{N}{M} \in ℤ)$
10	7 8 9	syl2anr	$⊢ (M \in ℕ \land N \in ℤ) \to (N \mod M = 0 \leftrightarrow \frac{N}{M} \in ℤ)$
11	6 10	bitr4d	$⊢ (M \in ℕ \land N \in ℤ) \to (M ∥ N \leftrightarrow N \mod M = 0)$