zmodfzo

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Assertion	zmodfzo	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 ..^B)$

Step	Hyp	Ref	Expression
1		zmodfz	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 \dots B - 1)$
2		nnz	$⊢ B \in ℕ \to B \in ℤ$
3		fzoval	$⊢ B \in ℤ \to (0 ..^B) = (0 \dots B - 1)$
4	2 3	syl	$⊢ B \in ℕ \to (0 ..^B) = (0 \dots B - 1)$
5	4	adantl	$⊢ (A \in ℤ \land B \in ℕ) \to (0 ..^B) = (0 \dots B - 1)$
6	1 5	eleqtrrd	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 ..^B)$

Metamath Proof Explorer