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


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