Metamath Proof Explorer

Theorem zmodidfzo

Description: Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018)

Ref Expression
Assertion zmodidfzo ⊢M∈ℤ∧N∈ℕ→MmodN=M↔M∈0..^N

Proof

Step Hyp Ref Expression
1 zmodid2 ⊢M∈ℤ∧N∈ℕ→MmodN=M↔M∈0…N−1
2 nnz ⊢N∈ℕ→N∈ℤ
3 fzoval ⊢N∈ℤ→0..^N=0…N−1
4 2 3 syl ⊢N∈ℕ→0..^N=0…N−1
5 4 adantl ⊢M∈ℤ∧N∈ℕ→0..^N=0…N−1
6 5 eqcomd ⊢M∈ℤ∧N∈ℕ→0…N−1=0..^N
7 6 eleq2d ⊢M∈ℤ∧N∈ℕ→M∈0…N−1↔M∈0..^N
8 1 7 bitrd ⊢M∈ℤ∧N∈ℕ→MmodN=M↔M∈0..^N