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 ) ) )