[proofplan] We use the order characterization on the integers: $x \le y$ precisely when $y-x$ is a nonnegative integer. [Translation invariance](/theorems/4911) follows by computing the difference after adding $c$ to both sides. Compatibility with multiplication by a nonnegative integer follows by rewriting the difference $bc-ac$ as $c(b-a)$ and using closure of the nonnegative integers under multiplication. [/proofplan] [step:Translate the inequality by comparing the resulting difference] Let $\mathbb{Z}_{\ge 0}$ denote the set of nonnegative integers. By the defining characterization of the order on $\mathbb{Z}$, for any $x,y \in \mathbb{Z}$, \begin{align*} x \le y \iff y-x \in \mathbb{Z}_{\ge 0}. \end{align*} Assume $a \le b$. Then $b-a \in \mathbb{Z}_{\ge 0}$. Using associativity and cancellation in the additive group of $\mathbb{Z}$, we compute \begin{align*} (b+c)-(a+c) = b-a. \end{align*} Since $b-a \in \mathbb{Z}_{\ge 0}$, it follows that \begin{align*} (b+c)-(a+c) \in \mathbb{Z}_{\ge 0}. \end{align*} Applying the order characterization again gives \begin{align*} a+c \le b+c. \end{align*} [/step] [step:Multiply the nonnegative difference by the nonnegative factor] Assume now that $a \le b$ and $0 \le c$. From $a \le b$ we have \begin{align*} b-a \in \mathbb{Z}_{\ge 0}. \end{align*} From $0 \le c$ we have \begin{align*} c \in \mathbb{Z}_{\ge 0}. \end{align*} The nonnegative integers are closed under multiplication, so \begin{align*} c(b-a) \in \mathbb{Z}_{\ge 0}. \end{align*} By distributivity and commutativity of multiplication in $\mathbb{Z}$, \begin{align*} c(b-a)=cb-ca=bc-ac. \end{align*} Therefore \begin{align*} bc-ac \in \mathbb{Z}_{\ge 0}. \end{align*} Applying the order characterization with $x=ac$ and $y=bc$ gives \begin{align*} ac \le bc. \end{align*} [guided] We again convert the order statement into a statement about a difference. The hypothesis $a \le b$ means, by the definition of the order on $\mathbb{Z}$, that the integer $b-a$ is nonnegative: \begin{align*} b-a \in \mathbb{Z}_{\ge 0}. \end{align*} The additional hypothesis $0 \le c$ means that $c$ itself is nonnegative: \begin{align*} c \in \mathbb{Z}_{\ge 0}. \end{align*} The goal is to prove $ac \le bc$. By the same order characterization, this is equivalent to proving that $bc-ac$ is nonnegative. The useful algebraic form of this difference is obtained by factoring out the common nonnegative factor $c$. Since $\mathbb{Z}$ is a commutative ring and multiplication distributes over subtraction, \begin{align*} bc-ac=cb-ca=c(b-a). \end{align*} Now both factors in $c(b-a)$ are nonnegative integers: $c \in \mathbb{Z}_{\ge 0}$ and $b-a \in \mathbb{Z}_{\ge 0}$. The set $\mathbb{Z}_{\ge 0}$ is closed under multiplication, hence \begin{align*} c(b-a) \in \mathbb{Z}_{\ge 0}. \end{align*} Using the equality $bc-ac=c(b-a)$, we obtain \begin{align*} bc-ac \in \mathbb{Z}_{\ge 0}. \end{align*} Therefore, by the definition of the order on $\mathbb{Z}$, \begin{align*} ac \le bc. \end{align*} [/guided] [/step]