Metamath Proof Explorer

Theorem zmodid2

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

Ref Expression
Assertion zmodid2 ⊢ M ∈ ℤ ∧ N ∈ ℕ → M mod N = M ↔ M ∈ 0 … N − 1

Proof

Step Hyp Ref Expression
1 zre ⊢ M ∈ ℤ → M ∈ ℝ
2 nnrp ⊢ N ∈ ℕ → N ∈ ℝ +
3 modid2 ⊢ M ∈ ℝ ∧ N ∈ ℝ + → M mod N = M ↔ 0 ≤ M ∧ M < N
4 1 2 3 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℕ → M mod N = M ↔ 0 ≤ M ∧ M < N
5 nnz ⊢ N ∈ ℕ → N ∈ ℤ
6 0z ⊢ 0 ∈ ℤ
7 elfzm11 ⊢ 0 ∈ ℤ ∧ N ∈ ℤ → M ∈ 0 … N − 1 ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
8 6 7 mpan ⊢ N ∈ ℤ → M ∈ 0 … N − 1 ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
9 3anass ⊢ M ∈ ℤ ∧ 0 ≤ M ∧ M < N ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
10 8 9 bitrdi ⊢ N ∈ ℤ → M ∈ 0 … N − 1 ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
11 5 10 syl ⊢ N ∈ ℕ → M ∈ 0 … N − 1 ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
12 ibar ⊢ M ∈ ℤ → 0 ≤ M ∧ M < N ↔ M ∈ ℤ ∧ 0 ≤ M ∧ M < N
13 12 bicomd ⊢ M ∈ ℤ → M ∈ ℤ ∧ 0 ≤ M ∧ M < N ↔ 0 ≤ M ∧ M < N
14 11 13 sylan9bbr ⊢ M ∈ ℤ ∧ N ∈ ℕ → M ∈ 0 … N − 1 ↔ 0 ≤ M ∧ M < N
15 4 14 bitr4d ⊢ M ∈ ℤ ∧ N ∈ ℕ → M mod N = M ↔ M ∈ 0 … N − 1