Nested quantifiers in an implication and its contrapositive I am working through a problem on implications, and I have confused myself.  I wish to state the contrapositive of:
$$\forall n\in \mathbb{Z}, \exists k \in \mathbb{N}, \ n \mid 12k+5 \wedge n \mid 18k+1 \implies n=17$$
My issue is with the nested quantifiers.  Does the existential quantifier belong to the hypothesis, and therefore the contrapositive is:
$$\forall n\in \mathbb{Z}, n \ne 17 \implies \forall k \in \mathbb{N}, n \nmid 12k+5 \vee n \nmid 18k+1$$
Alternatively, if the existential quantifier does not belong to the hypothesis, then the contrapositive should be:
$$\forall n\in \mathbb{Z}, \exists k\in \mathbb{N}, \ n \ne 17 \implies n \nmid 12k+5 \wedge n \nmid 18k+1$$
These are two VERY different statements, and both might be the wrong one.  What is the right answer here, and why?
 A: The logical form of your first statement is
$$\tag{1}
\forall n \in \mathbb{Z} \, \exists k \in \mathbb{N} ((n \mid 12k+5 \wedge n \mid 18k+1) \implies n=17)$$
The contrapositive of such a formula (obtained by reversing the arrow and negating its antecedent and consequent) is
$$\tag{2}\forall n \in \mathbb{Z} \, \exists k \in \mathbb{N} (n \neq 17 \implies (n\not \mid 12k+5 \lor n \not\mid 18k+1))$$
which is logically equivalent to
$$\tag{3}\forall n \in \mathbb{Z} (n \neq 17 \implies \exists k \in \mathbb{N}  (n\not \mid 12k+5 \lor n \not\mid 18k+1))$$
Note that both your proposals for the contrapositive are wrong, because they are not logically equivalent to $(2)$ or $(3)$. In your last formula you use $\land$ instead of $\lor$, and in your previous formula you use $\forall$ instead of $\exists$.

Another way to see this is considering the following formula, which is logically equivalent to $(1)$
$$\forall n \in \mathbb{Z} (\forall k \in \mathbb{N} (n \mid 12k+5 \wedge n \mid 18k+1) \implies n=17)$$
The contrapositive of such a formula (obtained by reversing the arrow and negating its antecedent and consequent) is exactly $(3)$.

The logical equivalences used above are:
\begin{align}
P \to Q &\equiv \lnot Q \to \lnot P &&\text{(contrapositive)}
\\
\lnot (P \land Q) &\equiv \lnot P \lor \lnot Q &&\text{(De Morgan)}
\\
\exists x (P \to Q) &\equiv (\forall x P) \to Q &&\text{(contravariance of the antecedent)}
\\
\exists x (Q \to P) &\equiv Q \to (\exists x P) &&\text{(covariance of the consequent)}
\end{align}
where, in the last  two equivalences, $x$ does not occur free in $Q$.
