Metamath Proof Explorer

Theorem zmodfz

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion zmodfz ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ 0 … B − 1

Proof

Step Hyp Ref Expression
1 zmodcl ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℕ 0
2 1 nn0zd ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℤ
3 1 nn0ge0d ⊢ A ∈ ℤ ∧ B ∈ ℕ → 0 ≤ A mod B
4 zre ⊢ A ∈ ℤ → A ∈ ℝ
5 nnrp ⊢ B ∈ ℕ → B ∈ ℝ +
6 modlt ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B < B
7 4 5 6 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B < B
8 0z ⊢ 0 ∈ ℤ
9 nnz ⊢ B ∈ ℕ → B ∈ ℤ
10 9 adantl ⊢ A ∈ ℤ ∧ B ∈ ℕ → B ∈ ℤ
11 elfzm11 ⊢ 0 ∈ ℤ ∧ B ∈ ℤ → A mod B ∈ 0 … B − 1 ↔ A mod B ∈ ℤ ∧ 0 ≤ A mod B ∧ A mod B < B
12 8 10 11 sylancr ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ 0 … B − 1 ↔ A mod B ∈ ℤ ∧ 0 ≤ A mod B ∧ A mod B < B
13 2 3 7 12 mpbir3and ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ 0 … B − 1