Metamath Proof Explorer


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 ..^ 𝐵 ) )