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 ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ 0 ..^ B

Proof

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