Is this an issue with the law of the excluded middle, or an issue with the proof? Part of a proof requiring you to prove that if $x^2$ is odd then $x$ is odd (given that $x \in \mathbb{N}$). It is my understanding that the contrapositive is used for this as follows.
$x=2n, n \in \mathbb{N}$
$\Rightarrow x^2 = 4n^2$
$\Rightarrow x^2$ is even
Then using the contrapositive:
$\Rightarrow \lnot Even(x^2) \rightarrow \lnot Even(x)$
Now the Law of the excluded middle:
$\Rightarrow Odd(x^2) \rightarrow Odd(x)$
So reasonably straight forward. However, my issue with this is whilst $x^2$ is even, it is even more strictly defined as a multiple of $4$. So in the contrapositive sense it doesn't feel right that it can be any even number. So what happens if that said number is 6? Not strictly divisible by 4 but still even. This is a bit difficult because this proof's conclusion is actually correct and any squared integer is either divible by 4 or odd. But that was found through exhaustion in a different way. Using the law of the excluded middle after saying that it wasn't just any even number seems spurious.
Could someone please clarify if I am right with reservation about this? If not, please explain (without just saying it is contrapositive, therefore). I feel like there should be a continuing connection between the definition of what type of even and what can be deduced from that.
 A: It is not a law of excluded middle that you need to prove that every integer is either even or odd.  Excluded middle applies equally to integers and reals, but not every real is even or odd.  To prove this property requires a property of integers, such as the division algorithm (divide by 2, look at remainder).
A: Let $(p(x)\equiv2\mid x), (q(x)\equiv2\mid x^2), (r(x)\equiv4\mid x^2)$.
Then we have
$$(\forall x\in\Bbb Z)\quad(2\mid x\implies4\mid x^2)$$
$\implies$
$$(\forall x\in\Bbb Z)\quad(2\mid x\implies(2\mid x^2\land 4\mid x^2))$$
$\implies$
$$(\forall x\in\Bbb Z)\quad(\neg (2\mid x^2\land 4\mid x^2) \implies 2\nmid x)$$
$\implies$
$$(\forall x\in\Bbb Z)\quad((2\nmid x^2\lor4\nmid x^2) \implies \neg 2\nmid x)$$
$\implies$
$$(\forall x\in\Bbb Z)\quad((2\nmid x^2 \implies 2\nmid x)\land(4\nmid x^2 \implies 2\nmid x))$$
$\implies$
$$(\forall x\in\Bbb Z)\quad(2\nmid x^2 \implies 2\nmid x)\land(\forall x\in\Bbb Z)\quad(4\nmid x^2 \implies 2\nmid x)$$
$\implies$
$$(\forall x\in\Bbb Z)\quad(2\nmid x^2 \implies 2\nmid x)$$

Now I think your confusion comes from considering $(\forall x\in\Bbb Z)\quad(4\nmid x^2 \implies 2\nmid x)$ which is also true.
Then $(4\nmid6)\implies(x^2=6\implies4\nmid x^2)$, and so we get
$$(\forall x\in\Bbb Z)\quad (x^2=6\implies4\nmid x^2\implies2\nmid x)$$
and we end up with the bizarre statement
$$(\forall x\in\Bbb Z)\quad(x^2=6\implies x\text{ is odd})$$
But of course, there is no such integer whose square is $6$ (and in fact, this is a valid proof of that being the case if we also use 'the square of an odd is odd').
For all integers, $x^2=6$ is false, and we can prove anything with a false premise. In general,
$$\neg P\implies(P\implies Q)$$
is true for any statements $P$ and $Q$.
A: Ignore the broader proof - do you agree with the assertion "If $x$ is divisible by $4$, then $x$ is even?" This is all that's going on. We're always allowed to "forget" information in a proof, and this has nothing to do with the excluded middle. When you conclude "$x^2$ is even," this in no way implies that you've concluded "$x^2$ is even and that's the most that can be said."
A: If you're in Paris, then you're in Europe. Even more particularly, you're in France. However, "if you're not in Europe, then you're not in Paris," is still a valid application of the contrapositive, even though we've "forgotten" the information about being in France.
"You're in Paris." $\longleftrightarrow  x$ is even.
"You're in Europe." $\longleftrightarrow  x^2$ is even.
"You're in France." $\longleftrightarrow  x^2$ is a multiple of $4$.
