Definition: When $a$ and $b$ are integers and $a$ is nonzero, $a$ divides $b$ means there is an integer $c$ such that $b=ac$ . Symbolically, $F((a,b))=\phantom{\mathrm{\exists }c\in \mathbb{Z}(b=ac)}$ and is a predicate over the domain Other (synonymous) ways to say that $F((a,b))$ is true:

When $a$ is a positive integer and $b$ is any integer, $a|b$ exactly when $b\mathbf{\text{ mod }}a=0$ When $a$ is a positive integer and $b$ is any integer, $a|b$ exactly $b=a\cdot (b\mathbf{\text{ div }}a)$