$\forall a,b,c \in \mathbb{N}\!:\ a\mid b \Rightarrow ac\mid bc. $ Divisibility Proof Could someone verify this proof?

Given the following definition of divisibility $(\forall{a,b \in \mathbb{N}})[a \mid b \equiv (\exists{c \in \mathbb{N}})(ac=b)]$.

Statement: $(\forall{a,b,c \in \mathbb{N}})[(a\mid b) \rightarrow (ac\mid bc)] $ .

Proof:

Let $a,b \in \mathbb{N}$ be arbitrary.  Assuming that $a\mid b$, we can conclude that $\exists{d \in \mathbb{N}}$ such that $ad = b$.  By Algebra we can deduce the following sequence of statements.  If $(ad)=b$, then $(ad)c=bc$.  Therefore $(ac)d=bc$.  Hence by the definition of divisibility we know that $ac\mid bc$.
Yes, your proof is correct. You might find it instructive to view the proof from a more conceptual viewpoint. Generally scaling a polynomial $f(x)$ by an invertible (so cancellable) element $c$ does not change its solution set since $c f(d) = 0 \iff f(d) = 0$. In particular the  solvability of $f(x) = 0$ is not altered - which is what we are concerned with for divisibility: $\,a\mid b\iff ax = b\,$ is solvable.

Let's consider the less trivial case of quadratic $f(x)$. The formula $g(a,b,c)$ for the solutions of a quadratic $ax^2+bx+c$ remains unaltered by nonzero coefficient scalings $g(ad,bd,cd) = g(a,b,c)$. As for solvability, scaling the polynomial by $d\neq 0$ multiplies the discriminant $b^2-4ac$ by $d^2$ so it does not affect the solvability criterion - that the discriminant be a perfect square. 

But we don't need to know these explicit (linear / quadratic) formulas  to deduce this. Rather, we can deduce it at a conceptually higher-level, simply from the cancellability of $\,c,\,$ i.e the invertibility of  scaling transformations $x\to cx$.

Remark $\ $ Below are some general remarks about such equational inferences.

Since the proof  employs only the associative and commutativite axioms for multiplication it remains true in any commutative semigroup. The proof employs only the inference rules of first-order equational logic, namely that equality is an equivalence relation (reflexive, symmetric, transitive) and the rules of substitution: $p(x) = q(x) \rightarrow p(a) = q(a)$ and replacement: $a = b \rightarrow p(a) = p(b)$.

By a famous theorem of Birkhoff, for any algebraic structure that can be defined by axioms - like comutativity, associativity, etc - that are all universally quantified equations, said inference rules are complete, i.e. an equation is provable from the axioms using said inference rules iff it is true in every structure that satisfies the axioms. However, finding such a purely equational proof can be highly difficult. For example, consider the famous Jacobson theorem that rings satisfying the axiom $x^n = x \;$ are commutative $xy = yx$.  It is  notoriously difficult for $n&gt;2$ to find purely equational proofs of this theorem. So ingenuity will be essential in general (e.g. exploiting innate structure such as the above equivalence under invertible scalings).
The proof is valid.