Metamath Proof Explorer

Theorem zmodid2

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

Ref Expression
Assertion zmodid2 ⊢M∈ℤ∧N∈ℕ→MmodN=M↔M∈0…N−1

Proof

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