# Metamath Proof Explorer

## Theorem zmodidfzo

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

Ref Expression
Assertion zmodidfzo ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0..^{N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 zmodid2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0\dots {N}-1\right)\right)$
2 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
3 fzoval ${⊢}{N}\in ℤ\to \left(0..^{N}\right)=\left(0\dots {N}-1\right)$
4 2 3 syl ${⊢}{N}\in ℕ\to \left(0..^{N}\right)=\left(0\dots {N}-1\right)$
5 4 adantl ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left(0..^{N}\right)=\left(0\dots {N}-1\right)$
6 5 eqcomd ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left(0\dots {N}-1\right)=\left(0..^{N}\right)$
7 6 eleq2d ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\in \left(0\dots {N}-1\right)↔{M}\in \left(0..^{N}\right)\right)$
8 1 7 bitrd ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0..^{N}\right)\right)$