zmodfz

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)

		Ref	Expression
	Assertion	zmodfz	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 \dots B - 1)$

Step	Hyp	Ref	Expression
1		zmodcl	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in ℕ_{0}$
2	1	nn0zd	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in ℤ$
3	1	nn0ge0d	$⊢ (A \in ℤ \land B \in ℕ) \to 0 \leq A \mod B$
4		zre	$⊢ A \in ℤ \to A \in ℝ$
5		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
6		modlt	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B < B$
7	4 5 6	syl2an	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B < B$
8		0z	$⊢ 0 \in ℤ$
9		nnz	$⊢ B \in ℕ \to B \in ℤ$
10	9	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to B \in ℤ$
11		elfzm11	$⊢ (0 \in ℤ \land B \in ℤ) \to (A \mod B \in (0 \dots B - 1) \leftrightarrow (A \mod B \in ℤ \land 0 \leq A \mod B \land A \mod B < B))$
12	8 10 11	sylancr	$⊢ (A \in ℤ \land B \in ℕ) \to (A \mod B \in (0 \dots B - 1) \leftrightarrow (A \mod B \in ℤ \land 0 \leq A \mod B \land A \mod B < B))$
13	2 3 7 12	mpbir3and	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 \dots B - 1)$

Metamath Proof Explorer