# Metamath Proof Explorer

## Theorem zmodid2

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

Ref Expression
Assertion zmodid2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0\dots {N}-1\right)\right)$

### Proof

Step Hyp Ref Expression
1 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
2 nnrp ${⊢}{N}\in ℕ\to {N}\in {ℝ}^{+}$
3 modid2 ${⊢}\left({M}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left({M}\mathrm{mod}{N}={M}↔\left(0\le {M}\wedge {M}<{N}\right)\right)$
4 1 2 3 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔\left(0\le {M}\wedge {M}<{N}\right)\right)$
5 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
6 0z ${⊢}0\in ℤ$
7 elfzm11 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\in \left(0\dots {N}-1\right)↔\left({M}\in ℤ\wedge 0\le {M}\wedge {M}<{N}\right)\right)$
8 6 7 mpan ${⊢}{N}\in ℤ\to \left({M}\in \left(0\dots {N}-1\right)↔\left({M}\in ℤ\wedge 0\le {M}\wedge {M}<{N}\right)\right)$
9 3anass ${⊢}\left({M}\in ℤ\wedge 0\le {M}\wedge {M}<{N}\right)↔\left({M}\in ℤ\wedge \left(0\le {M}\wedge {M}<{N}\right)\right)$
10 8 9 syl6bb ${⊢}{N}\in ℤ\to \left({M}\in \left(0\dots {N}-1\right)↔\left({M}\in ℤ\wedge \left(0\le {M}\wedge {M}<{N}\right)\right)\right)$
11 5 10 syl ${⊢}{N}\in ℕ\to \left({M}\in \left(0\dots {N}-1\right)↔\left({M}\in ℤ\wedge \left(0\le {M}\wedge {M}<{N}\right)\right)\right)$
12 ibar ${⊢}{M}\in ℤ\to \left(\left(0\le {M}\wedge {M}<{N}\right)↔\left({M}\in ℤ\wedge \left(0\le {M}\wedge {M}<{N}\right)\right)\right)$
13 12 bicomd ${⊢}{M}\in ℤ\to \left(\left({M}\in ℤ\wedge \left(0\le {M}\wedge {M}<{N}\right)\right)↔\left(0\le {M}\wedge {M}<{N}\right)\right)$
14 11 13 sylan9bbr ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\in \left(0\dots {N}-1\right)↔\left(0\le {M}\wedge {M}<{N}\right)\right)$
15 4 14 bitr4d ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0\dots {N}-1\right)\right)$