$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\notag \\ #1 \quad & \quad \text{"#2"} \notag \\ \quad & }
\newcommand{\endcalc}{\notag \end{align}}
$This is not a direct answer, but here is an alternative proof which might be helpful.
Put slightly more formally, and implicitly assuming that all variables range over $\;\mathbb Z\;$, you're asked to prove
$$
\langle \forall k : k > 0 : b \not\mid k \rangle \;\Rightarrow\; b = 0
$$
for all $\;b\;$.
So let's calculate:
$$\calc
\langle \forall k : k > 0 : b \not\mid k \rangle
\calcop{\equiv}{definition of $\;\mid\;$}
\langle \forall k : k > 0 : \lnot \langle \exists n :: n \times b = k \rangle \rangle
\calcop{\equiv}{logic: DeMorgan; merge $\;\forall\;$ quantifications}
\langle \forall k,n : k > 0 : n \times b \not= k \rangle
\calcop{\equiv}{logic: transpose; split $\;\forall\;$ quantifications -- preparing for next step}
\langle \forall n :: \langle \forall k : n \times b = k : k \leq 0 \rangle \rangle
\calcop{\equiv}{logic: one-point rule}
\langle \forall n :: n \times b \leq 0 \rangle
\calcop{(*) \;\;\;\ \equiv}{arithmetic -- split cases to separate $\;n,b\;$}
\langle \forall n :: (n \leq 0 \lor b \leq 0) \;\land\; (n \geq 0 \lor b \geq 0) \rangle
\calcop{\equiv}{logic: $\;\forall\;$ distributes over $\;\land\;$}
\langle \forall n :: n \leq 0 \lor b \leq 0 \rangle \;\land\; \langle \forall n :: n \geq 0 \lor b \geq 0 \rangle
\calcop{\equiv}{logic: pull part not using $\;n\;$ outside of $\;\forall n\;$, twice}
(\langle \forall n :: n \leq 0 \rangle \lor b \leq 0) \;\land\; (\langle \forall n :: n \geq 0 \rangle \lor b \geq 0)
\calcop{\equiv}{$\;\langle \forall n :: n \leq 0 \rangle\;$ and $\;\langle \forall n :: n \geq 0 \rangle\;$ are false; simplify}
b \leq 0 \;\land\; b \geq 0
\calcop{\equiv}{arithmetic}
b = 0
\endcalc$$
Notes. Many readers will probably find this proof overly long and formal, however, I consider it to be straightforward to design, because the design is guided by the shape of the formulas, together with the goal that we work towards.
This is an example of a proof which minimizes the number of surprises or 'rabbits pulled out of a hat': almost every step is really the simplest thing that one could do. And it would have been shorter, if I could assume that all readers would be familiar with using logic, as promoted by people like Edsger W. Dijkstra and David Gries and Fred B. Schneider.
The step where we have the most choice is $(*)$. There I could also have chosen the alternative
$$
n \times b \leq 0 \;\equiv\; (n \leq 0 \land b \geq 0) \;\lor\; (n \geq 0 \land b \leq 0)
$$
However, I chose
$$
n \times b \leq 0 \;\equiv\; (n \leq 0 \lor b \leq 0) \;\land\; (n \geq 0 \lor b \geq 0)
$$
because the latter has the form $\;P \land Q\;$, so that I could distribute $\;\forall\;$ over it in the next step. The alternative would have required to introduce a $\;\Rightarrow\;$ step, making the proof less general.
Finally, note that three notation decisions were helpful: assuming all variables are integers avoids $\;\in \mathbb Z\;$ throughout, reducing the visual noise; writing out the $\;\forall k\;$ quantification explicitly made it possible to manipulate it explicitly and apply the one-point rule; and expressions of the form $\;\ldots > 0\;$ are a lot easier to manipulate than $\;\ldots \in \mathbb N\;$ (or $\;\mathbb N^+\;$).