zmodcl

Description: Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008)

		Ref	Expression
	Assertion	zmodcl	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
3		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
4	1 2 3	syl2an	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
5		nnz	$⊢ B \in ℕ \to B \in ℤ$
6	5	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℤ$
7		nndivre	$⊢ (A \in ℝ \land B \in ℕ) \to \frac{A}{B} \in ℝ$
8	1 7	sylan	$⊢ (A \in ℤ \land B \in ℕ) \to \frac{A}{B} \in ℝ$
9	8	flcld	$⊢ (A \in ℤ \land B \in ℕ) \to ⌊\frac{A}{B}⌋ \in ℤ$
10	6 9	zmulcld	$⊢ (A \in ℤ \land B \in ℕ) \to B ⌊\frac{A}{B}⌋ \in ℤ$
11		zsubcl	$⊢ (A \in ℤ \land B ⌊\frac{A}{B}⌋ \in ℤ) \to A - B ⌊\frac{A}{B}⌋ \in ℤ$
12	10 11	syldan	$⊢ (A \in ℤ \land B \in ℕ) \to A - B ⌊\frac{A}{B}⌋ \in ℤ$
13	4 12	eqeltrd	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in ℤ$
14		modge0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to 0 \leq A \mod B$
15	1 2 14	syl2an	$⊢ (A \in ℤ \land B \in ℕ) \to 0 \leq A \mod B$
16		elnn0z	$⊢ A \mod B \in ℕ_{0} \leftrightarrow (A \mod B \in ℤ \land 0 \leq A \mod B)$
17	13 15 16	sylanbrc	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in ℕ_{0}$

Metamath Proof Explorer