Theorem 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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ( 0 ..^ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		zmodfz	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ( 0 ... ( 𝐵 − 1 ) ) )
2		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
3		fzoval	⊢ ( 𝐵 ∈ ℤ → ( 0 ..^ 𝐵 ) = ( 0 ... ( 𝐵 − 1 ) ) )
4	2 3	syl	⊢ ( 𝐵 ∈ ℕ → ( 0 ..^ 𝐵 ) = ( 0 ... ( 𝐵 − 1 ) ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 0 ..^ 𝐵 ) = ( 0 ... ( 𝐵 − 1 ) ) )
6	1 5	eleqtrrd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 mod 𝐵 ) ∈ ( 0 ..^ 𝐵 ) )