This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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