# Metamath Proof Explorer

## Theorem zmodidfzoimp

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

Ref Expression
Assertion zmodidfzoimp ${⊢}{M}\in \left(0..^{N}\right)\to {M}\mathrm{mod}{N}={M}$

### Proof

Step Hyp Ref Expression
1 elfzo0 ${⊢}{M}\in \left(0..^{N}\right)↔\left({M}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {M}<{N}\right)$
2 nn0z ${⊢}{M}\in {ℕ}_{0}\to {M}\in ℤ$
3 2 anim1i ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in ℕ\right)\to \left({M}\in ℤ\wedge {N}\in ℕ\right)$
4 3 3adant3 ${⊢}\left({M}\in {ℕ}_{0}\wedge {N}\in ℕ\wedge {M}<{N}\right)\to \left({M}\in ℤ\wedge {N}\in ℕ\right)$
5 1 4 sylbi ${⊢}{M}\in \left(0..^{N}\right)\to \left({M}\in ℤ\wedge {N}\in ℕ\right)$
6 zmodidfzo ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\mathrm{mod}{N}={M}↔{M}\in \left(0..^{N}\right)\right)$
7 6 biimprd ${⊢}\left({M}\in ℤ\wedge {N}\in ℕ\right)\to \left({M}\in \left(0..^{N}\right)\to {M}\mathrm{mod}{N}={M}\right)$
8 5 7 mpcom ${⊢}{M}\in \left(0..^{N}\right)\to {M}\mathrm{mod}{N}={M}$