Metamath Proof Explorer

Theorem zmodcl

Description: Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008)

Ref Expression
Assertion zmodcl ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 zre ⊢ A ∈ ℤ → A ∈ ℝ
2 nnrp ⊢ B ∈ ℕ → B ∈ ℝ +
3 modval ⊢ A ∈ ℝ ∧ B ∈ ℝ + → A mod B = A − B ⁢ A B
4 1 2 3 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B = A − B ⁢ A B
5 nnz ⊢ B ∈ ℕ → B ∈ ℤ
6 5 adantl ⊢ A ∈ ℤ ∧ B ∈ ℕ → B ∈ ℤ
7 nndivre ⊢ A ∈ ℝ ∧ B ∈ ℕ → A B ∈ ℝ
8 1 7 sylan ⊢ A ∈ ℤ ∧ B ∈ ℕ → A B ∈ ℝ
9 8 flcld ⊢ A ∈ ℤ ∧ B ∈ ℕ → A B ∈ ℤ
10 6 9 zmulcld ⊢ A ∈ ℤ ∧ B ∈ ℕ → B ⁢ A B ∈ ℤ
11 zsubcl ⊢ A ∈ ℤ ∧ B ⁢ A B ∈ ℤ → A − B ⁢ A B ∈ ℤ
12 10 11 syldan ⊢ A ∈ ℤ ∧ B ∈ ℕ → A − B ⁢ A B ∈ ℤ
13 4 12 eqeltrd ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℤ
14 modge0 ⊢ A ∈ ℝ ∧ B ∈ ℝ + → 0 ≤ A mod B
15 1 2 14 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℕ → 0 ≤ A mod B
16 elnn0z ⊢ A mod B ∈ ℕ 0 ↔ A mod B ∈ ℤ ∧ 0 ≤ A mod B
17 13 15 16 sylanbrc ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℕ 0