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