Metamath Proof Explorer

Theorem zmodfzp1

Description: An integer mod B lies in the first B + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018)

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

Step	Hyp	Ref	Expression
1		fzossfz	$⊢ (0 ..^B) \subseteq (0 \dots B)$
2		zmodfzo	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 ..^B)$
3	1 2	sseldi	$⊢ (A \in ℤ \land B \in ℕ) \to A \mod B \in (0 \dots B)$