Negation of divisibility I cannot find the error

Question

First, for any natural integers $x$ and $y$, we define $x\mid y$ by :

$\exists k\in\mathbb{Z},y=kx$

We can then define the negation of the divisibility $x\nmid y$ by :

$\neg(\exists k\in\mathbb{Z},y=kx)$

Which is equivalent to :

$\forall k\in\mathbb{Z},y\neq kx$

---

Let $(a,b)\in\mathbb{N}^*$. We want to show the statement :

$a\nmid b\Rightarrow a\nmid b^2$

We suppose that $a\nmid b$. By definition of the negation of the divisibility, we have :

$\forall k\in\mathbb{Z},b\neq ka$

By universal instantiation, we can use a variable $k$ such that :

$b\neq ka$

We can then multiply by $b$ :

$b^2\neq b(ka)$

And by associativity of the multiplication we have :

$b^2\neq (bk)a$

We can then take $k'=bk$, and we have :

$b^2\neq k'a$

Then, by universal generalization :

$\forall k'\in\mathbb{Z},b^2\neq k'a$

And by definition of the negation of the divibility :

$a\nmid b^2$

We can then deduce that : $a\nmid b\Rightarrow a\nmid b^2$

---

But I can construct a counterexample, for instance $a=9$ and $b=3$. We clearly have $9\nmid 3$ but we have $9\nmid 9$.

I think maybe the problem lie by taking $k'$ and an incorrect usage of universal generalization rule, but I do not understand why.

Answer 1

$k’$ is an arbitrary multiple of the constant $b,$ so it is not an arbitrary integer. So, instead of $$\forall k'{\in}\mathbb{Z}\:b^2\neq k'a,$$ you can infer only that $$\forall k{\in}\mathbb{Z}\:(b^2\neq kab)$$ or, equivalently,$$\forall k{,}k'{\in}\mathbb{Z}\:(k’=kb\implies b^2\neq k'a).$$

---

Addendum

If you can write $k'=kb\Rightarrow b^2\neq k'a,$ it means that $k'=kb$ was an undischarged assumption ? So I cannot apply universal generalization rule because of this ?

Yes, exactly.