This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zmodcld

Description: Closure law for the modulo operation restricted to integers. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses zmodcld.1 ⊢ φ → A ∈ ℤ
zmodcld.2 ⊢ φ → B ∈ ℕ
Assertion zmodcld ⊢ φ → A mod B ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 zmodcld.1 ⊢ φ → A ∈ ℤ
2 zmodcld.2 ⊢ φ → B ∈ ℕ
3 zmodcl ⊢ A ∈ ℤ ∧ B ∈ ℕ → A mod B ∈ ℕ 0
4 1 2 3 syl2anc ⊢ φ → A mod B ∈ ℕ 0