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 ∈ ℕ → M mod N = M ↔ M ∈ 0 ..^ N

Proof

Step Hyp Ref Expression
1 zmodid2 ⊢ M ∈ ℤ ∧ N ∈ ℕ → M mod N = 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 ∈ ℕ → M mod N = M ↔ M ∈ 0 ..^ N