Metamath Proof Explorer


Theorem zmodid2

Description: Identity law for modulo restricted to integers. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion zmodid2 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
3 modid2 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
4 1 2 3 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀 ↔ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
5 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
6 0z 0 ∈ ℤ
7 elfzm11 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
8 6 7 mpan ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
9 3anass ( ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀𝑀 < 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
10 8 9 bitrdi ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) ) )
11 5 10 syl ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) ) )
12 ibar ( 𝑀 ∈ ℤ → ( ( 0 ≤ 𝑀𝑀 < 𝑁 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) ) )
13 12 bicomd ( 𝑀 ∈ ℤ → ( ( 𝑀 ∈ ℤ ∧ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) ↔ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
14 11 13 sylan9bbr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ↔ ( 0 ≤ 𝑀𝑀 < 𝑁 ) ) )
15 4 14 bitr4d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 mod 𝑁 ) = 𝑀𝑀 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )