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

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