Metamath Proof Explorer

Theorem zmodidfzoimp

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

Ref Expression
Assertion zmodidfzoimp ⊢ M ∈ 0 ..^ N → M mod N = M

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ M ∈ 0 ..^ N ↔ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ M < N
2 nn0z ⊢ M ∈ ℕ 0 → M ∈ ℤ
3 2 anim1i ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ → M ∈ ℤ ∧ N ∈ ℕ
4 3 3adant3 ⊢ M ∈ ℕ 0 ∧ N ∈ ℕ ∧ M < N → M ∈ ℤ ∧ N ∈ ℕ
5 1 4 sylbi ⊢ M ∈ 0 ..^ N → M ∈ ℤ ∧ N ∈ ℕ
6 zmodidfzo ⊢ M ∈ ℤ ∧ N ∈ ℕ → M mod N = M ↔ M ∈ 0 ..^ N
7 6 biimprd ⊢ M ∈ ℤ ∧ N ∈ ℕ → M ∈ 0 ..^ N → M mod N = M
8 5 7 mpcom ⊢ M ∈ 0 ..^ N → M mod N = M